# HG changeset patch # User haftmann # Date 1283522899 -7200 # Node ID 91d2a9844d574f89b9f01357860916e25fff1193 # Parent 240e2b41a041e238b7a0fd2516700e485157c99a# Parent 6f6a9c8abbacfcfaf1501faaab7efba15aaa7fb6 merged diff -r 240e2b41a041 -r 91d2a9844d57 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Fri Sep 03 14:20:47 2010 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Fri Sep 03 16:08:19 2010 +0200 @@ -60,6 +60,6 @@ CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" -FULL_CMD="quick_and_dirty := QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" +FULL_CMD="quick_and_dirty := $QND_FLAG; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1