build browser more robustly before startup;
authorwenzelm
Wed, 09 Jan 2013 14:01:50 +0100
changeset 50782 a26f7cf81d2f
parent 50781 a0f22c2d60cc
child 50783 8f42d300748f
build browser more robustly before startup;
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 09 13:38:57 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 09 14:01:50 2013 +0100
@@ -185,6 +185,7 @@
 ## dependencies
 
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+  "$ISABELLE_TOOL" browser -b || exit $?
   if [ "$BUILD_JARS" = jars_fresh ]; then
     "$ISABELLE_TOOL" graphview -b -f || exit $?
   else