# HG changeset patch
# User wenzelm
# Date 1316779929 -7200
# Node ID bbd7eac14df3502db1ae972fb6bd12542331cecf
# Parent  55274f7e306bb2dfa6b7930e91de50bfd13782a8
augment existing print mode;

diff -r 55274f7e306b -r bbd7eac14df3 bin/isabelle-process
--- a/bin/isabelle-process	Fri Sep 23 13:44:31 2011 +0200
+++ b/bin/isabelle-process	Fri Sep 23 14:12:09 2011 +0200
@@ -212,7 +212,7 @@
 
 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
 
-[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
+[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
 
 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"