disabled old jedit plugin;
authorwenzelm
Sun Dec 28 23:20:57 2008 +0100 (2008-12-28)
changeset 291863d25e96ceb98
parent 29185 26fcfca1db9d
child 29188 ff41885a1234
disabled old jedit plugin;
Admin/build
     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