| changeset 53386 | 16696e649fea |
| parent 47517 | 6bc4c66d8c1b |
| child 53392 | a1a45fdc53a3 |
--- a/src/HOL/TPTP/lib/Tools/tptp_graph Tue Sep 03 21:46:40 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph Tue Sep 03 21:46:40 2013 +0100 @@ -143,8 +143,8 @@ cd $WORKDIR if [ -z "$NON_EXEC" ]; then $DOT -Txdot "${FILENAME}.dot" \ - | $DOT2TEX -f pgf -t raw --crop > "${FILENAME}.tex" - $PERL -w -p -e 's/_/\\_/g' "${FILENAME}.tex" + | $DOT2TEX -f pgf -t raw --crop \ + | $PERL -w -p -e 's/_/\\_/g' > "${FILENAME}.tex" fi if [ "$OUTPUT_FORMAT" -eq 1 ]; then