# HG changeset patch
# User blanchet
# Date 1378991694 -7200
# Node ID 778b2b8f4a352ec98ffbf6cb5ed8ce6fe0b78f0a
# Parent  fc5167ee9111b92329eb122272ce5afbc97739f7
more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses

diff -r fc5167ee9111 -r 778b2b8f4a35 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 15:14:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Sep 12 15:14:54 2013 +0200
@@ -166,7 +166,7 @@
     val core = "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file
     val command =
       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
-      \python -B ./mash.py --quiet\
+      \PYTHONDONTWRITEBYTECODE=y ./mash.py --quiet\
       \ --outputDir " ^ model_dir ^
       " --modelFile=" ^ model_dir ^ "/model.pickle\
       \ --dictsFile=" ^ model_dir ^ "/dict.pickle\