Admin/build

--- a/Admin/build	Sun Dec 28 20:25:39 2008 +0100
+++ b/Admin/build	Sun Dec 28 23:20:57 2008 +0100
@@ -101,15 +101,6 @@
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
   popd >/dev/null
-
-  if [ -d "$HOME/lib/jedit/current" ]; then
-    pushd "$ISABELLE_HOME/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
 }