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