1 # Dave Mason's option to specify a different stylesheet
10 echo "Usage: `basename $0` [filename.sgml]" >&2
14 output="`echo $1 | sed 's,\.sgml$,.ps,;s,\.sgm$,.ps,'`"
15 outdvi="`echo $1 | sed 's,\.sgml$,.dvi,;s,\.sgm$,.dvi,'`"
17 dvips $outdvi -o $output