#!/bin/sh INPUT="$1" OUTPUT="$2" if test -z "$INPUT" -o -z "$OUTPUT"; then echo "usage: $0 " exit 1 fi HEADER='ArangoDB Manual

' FOOTER='

' sed -e "s~ ~${HEADER}~" $INPUT \ | sed -e "s~ ~${FOOTER}~" \ | sed -e "s~

\$[^<]*\$

\\1

~" > $OUTPUT