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 446728ba759b8caa8
parent 44671 bfad30568d40
child 44673 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
     1.1 --- a/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Wed Jul 13 22:16:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/lib/Tools/nitrox	Wed Jul 13 22:16:19 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  for FILE in "$@"
     1.6  do
     1.7 -  (echo "theory Nitrox_Run imports Main begin" &&
     1.8 -   echo "ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *}" &&
     1.9 -   echo "end;") | isabelle tty
    1.10 +  echo "theory Scratch imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
    1.11 +    > /tmp/$ISABELLE_TMP/Scratch.thy
    1.12 +  $ISABELLE_PROCESS -e "use_thy \"/tmp/$ISABELLE_TMP/Scratch\"; exit 1;"
    1.13  done