src/HOL/TPTP/lib/Tools/tptp_graph
changeset 53386 16696e649fea
parent 47517 6bc4c66d8c1b
child 53392 a1a45fdc53a3
equal deleted inserted replaced
53385:7edd43d0c0ba 53386:16696e649fea
   141 
   141 
   142 [ -z "$NON_EXEC" ] && generate_dot $1 "$WORKDIR/${FILENAME}.dot"
   142 [ -z "$NON_EXEC" ] && generate_dot $1 "$WORKDIR/${FILENAME}.dot"
   143 cd $WORKDIR
   143 cd $WORKDIR
   144 if [ -z "$NON_EXEC" ]; then
   144 if [ -z "$NON_EXEC" ]; then
   145   $DOT -Txdot "${FILENAME}.dot" \
   145   $DOT -Txdot "${FILENAME}.dot" \
   146   | $DOT2TEX -f pgf -t raw --crop > "${FILENAME}.tex"
   146   | $DOT2TEX -f pgf -t raw --crop \
   147   $PERL -w -p -e 's/_/\\_/g' "${FILENAME}.tex"
   147   | $PERL -w -p -e 's/_/\\_/g' > "${FILENAME}.tex"
   148 fi
   148 fi
   149 
   149 
   150 if [ "$OUTPUT_FORMAT" -eq 1 ]; then
   150 if [ "$OUTPUT_FORMAT" -eq 1 ]; then
   151   TARGET=$FILENAME.tex
   151   TARGET=$FILENAME.tex
   152 else
   152 else