avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
authorblanchet
Wed, 13 Jul 2011 22:16:19 +0200
changeset 43808 8ba759b8caa8
parent 43807 bfad30568d40
child 43809 151288f723dc
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
src/HOL/Tools/Nitpick/lib/Tools/nitrox
--- a/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Wed Jul 13 22:16:19 2011 +0200
+++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Wed Jul 13 22:16:19 2011 +0200
@@ -20,7 +20,7 @@
 
 for FILE in "$@"
 do
-  (echo "theory Nitrox_Run imports Main begin" &&
-   echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
-   echo "end;") | isabelle tty
+  echo "theory Scratch imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
+    > /tmp/$ISABELLE_TMP/Scratch.thy
+  $ISABELLE_PROCESS -e "use_thy \"/tmp/$ISABELLE_TMP/Scratch\"; exit 1;"
 done