7 dir=`echo "$option" | sed 's/^-dest://'`
8 cmd_line="$cmd_line -o \"$dir\""
11 cmd_line="$cmd_line --default-template"
14 ext=`echo "$option" | sed 's/^-ext://'`
15 cmd_line="$cmd_line --ext=$ext"
21 s=`echo "$option" | sed 's/^-source://'`
22 cmd_line="$cmd_line $s"
25 template=`echo "$option" | sed 's/^-template://'`
26 cmd_line="$cmd_line --template=$template"
32 cmd_line="$cmd_line $option"
37 exec mdoc export-html $cmd_line