1.1 --- a/Admin/build Sun Dec 28 20:25:39 2008 +0100
1.2 +++ b/Admin/build Sun Dec 28 23:20:57 2008 +0100
1.3 @@ -101,15 +101,6 @@
1.4 pushd "$ISABELLE_HOME/src/Pure" >/dev/null
1.5 "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
1.6 popd >/dev/null
1.7 -
1.8 - if [ -d "$HOME/lib/jedit/current" ]; then
1.9 - pushd "$ISABELLE_HOME/lib/jedit/plugin" >/dev/null
1.10 - ./mk
1.11 - [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
1.12 - popd >/dev/null
1.13 - else
1.14 - echo "Warning: skipping jedit plugin"
1.15 - fi
1.16 }
1.17
1.18