#! /bin/bash -e
# Last edited on 2017-04-23 19:39:39 by jstolfi

usage="$0 [ -landscape | -portrait ] [ -8pt|-9pt|-10pt|-11pt|-12pt|-14pt|-17pt|-20pt ] [ -twocolumn ] < INFILE.iso > OUTFILE.ps"

name="/tmp/itp$$"

err="${name}.err"
ps="${name}.ps"

${STOLFIHOME}/lib/do-iso-to-ps ${name} $* 

if [[ -s ${err} ]]; then
  cat ${err} 1>&2
  /bin/rm ${err}
elif [[ -s ${ps} ]]; then
  echo "postscript generated ${ps}" 1>&2
  /bin/cat ${ps}
else
  echo "command failed" 1>&2
fi
#/bin/rm -f ${name}.{ps,dvi,aux,log,err}