+</html>'
+
+# substitute the pattern $1 by the content of the file $2
+subst() {
+ awk -v pat="$1" -v rep="$(sed 's:\\:\\\\:g' $2)" '{gsub(pat,rep);gsub(pat,"\\&");print}'
+}
+
+# update the date field of file $1
+updadate() {
+ local x=$1
+ local t=$(git log -n 1 --format=%ct $x)
+ [[ -n "$t" ]] || t=$(stat -c %Y $x)
+ local d=$(LANG= date -d @$t +"%d %B %Y")
+ sed -i "s/^\( Date: *\).*/\1$d/" $x