diff options
| -rwxr-xr-x | scripts/mkwebpage | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/scripts/mkwebpage b/scripts/mkwebpage index 10d170c79..133263dc7 100755 --- a/scripts/mkwebpage +++ b/scripts/mkwebpage @@ -11,8 +11,8 @@ set -e extract_date () { # This strange construct is to speed up things. Grouping a "s" and a "q" # does not work. Anyway we should use awk instead. - sed '/^.*\$Id$.*$/q' $1 | - sed -n 's!^.*\$Id$!\1-\2-\3 \4!p' + sed '/^.*\$\[I\]d:.*\$.*$/q' $1 | + sed -n 's!^.*\$\[I\]d: [^ ]\+ [^ ]\+ \([0-9]*\)/\([0-9]*\)/\([0-9]*\) [^ ]\+ \([^ ]\+\).*$!\1-\2-\3 \4!p' } # We have to edit most files |