# HG changeset patch
# User wenzelm
# Date 1216458318 -7200
# Node ID cf0c60e821bb1aaa75b5f9ca310df988ad74c2ef
# Parent  0f8e2dcabbf90411432e73547bb60aa44668c1e1
build jedit plugin only if jedit is available;

diff -r 0f8e2dcabbf9 -r cf0c60e821bb Admin/build
--- a/Admin/build	Fri Jul 18 22:03:20 2008 +0200
+++ b/Admin/build	Sat Jul 19 11:05:18 2008 +0200
@@ -123,11 +123,15 @@
   [ -f isabelle.jar ] || fail "Failed to build Isabelle process wrapper!"
   popd >/dev/null
 
-  type -p scalac >/dev/null || fail "Scala compiler unavailable"
-  pushd lib/jedit/plugin >/dev/null
-  ./mk
-  [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
-  popd >/dev/null
+  if [ -d "$HOME/lib/jedit/current" ]; then
+    type -p scalac >/dev/null || fail "Scala compiler unavailable"
+    pushd lib/jedit/plugin >/dev/null
+    ./mk
+    [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
+    popd >/dev/null
+  else
+    echo "Warning: skipping jedit plugin"
+  fi
 }