enforce fonts;
authorwenzelm
Fri, 28 Jan 2011 11:19:12 +0100
changeset 41642 b9442d9ce7f5
parent 41641 f7efeb18c07e
child 41643 10b0d338d99e
enforce fonts;
Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Thu Jan 27 20:50:58 2011 +0100
+++ b/Admin/MacOS/App1/script	Fri Jan 28 11:19:12 2011 +0100
@@ -54,6 +54,22 @@
 fi
 
 
+# enforce fonts
+
+if [ ! -f "$HOME/Library/Fonts/IsabelleText.ttf" -o ! -f "$HOME/Library/Fonts/IsabelleTextBold.ttf" ]
+then
+  cp -f "$THIS/Isabelle/lib/fonts/IsabelleText.ttf" "$HOME/Library/Fonts/"
+  cp -f "$THIS/Isabelle/lib/fonts/IsabelleTextBold.ttf" "$HOME/Library/Fonts/"
+  sleep 3
+fi
+
+EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="-x"
+EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="true"
+
+EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="-f"
+EMACS_OPTIONS["${#EMACS_OPTIONS[@]}"]="IsabelleText"
+
+
 # run interface with error feedback
 
 OUTPUT="/tmp/isabelle$$.out"