author | sultana |
Tue, 03 Sep 2013 21:46:40 +0100 | |
changeset 53386 | 16696e649fea |
parent 53385 | 7edd43d0c0ba |
child 53387 | ea754ae93b55 |
--- 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