# HG changeset patch
# User sultana
# Date 1378241200 -3600
# Node ID 16696e649feae637dde4344191506b4cfb3341f3
# Parent  7edd43d0c0bad564343b6b9349b0ddc07ab2c54b
corrected syntax filter;

diff -r 7edd43d0c0ba -r 16696e649fea src/HOL/TPTP/lib/Tools/tptp_graph
--- 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