# HG changeset patch
# User wenzelm
# Date 1357736510 -3600
# Node ID a26f7cf81d2f416d12087ca6866db80164a62224
# Parent  a0f22c2d60ccd4f815cdd6d05a96bd11bda6cd0d
build browser more robustly before startup;

diff -r a0f22c2d60cc -r a26f7cf81d2f 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