# HG changeset patch
# User wenzelm
# Date 1368810663 -7200
# Node ID 69137d20ab0b2b853d1b947f615911ec6d11055f
# Parent  fc458f304f93211220cb806f4e226cc3d68dde5b
more system-atic options;

diff -r fc458f304f93 -r 69137d20ab0b src/Tools/WWW_Find/Start_WWW_Find.thy
--- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Fri May 17 19:04:52 2013 +0200
+++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Fri May 17 19:11:03 2013 +0200
@@ -5,7 +5,6 @@
 theory Start_WWW_Find imports WWW_Find begin
 
 ML {*
-  Options.default_put_bool @{option show_question_marks} false;
   YXML_Find_Theorems.init ();
   val port = Markup.parse_int (getenv "SCGIPORT");
   ScgiServer.server' 10 "/" port;
diff -r fc458f304f93 -r 69137d20ab0b src/Tools/WWW_Find/lib/Tools/wwwfind
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Fri May 17 19:04:52 2013 +0200
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Fri May 17 19:11:03 2013 +0200
@@ -134,10 +134,10 @@
     "$LIGHTTPD" -f "$WWWCONFIG"
     if [ "$LOGFILE" = true ]; then
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" "$INPUT") &
+       nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" "$INPUT") &
     else
       (cd "$WWWFINDDIR"; \
-       nohup "$ISABELLE_PROCESS" -r -e "$MLSTARTSERVER" \
+       nohup "$ISABELLE_PROCESS" -r -o show_question_marks=false -e "$MLSTARTSERVER" \
          "$INPUT" > /dev/null 2> /dev/null) &
     fi
     ;;