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