# HG changeset patch
# User wenzelm
# Date 1230502857 -3600
# Node ID 3d25e96ceb9812da209a8cd61b89f106fe009c24
# Parent  26fcfca1db9df242f621aa874a5cccd74917d3da
disabled old jedit plugin;

diff -r 26fcfca1db9d -r 3d25e96ceb98 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
 }