equal
deleted
inserted
replaced
99 type -p scalac >/dev/null || fail "Scala compiler unavailable" |
99 type -p scalac >/dev/null || fail "Scala compiler unavailable" |
100 |
100 |
101 pushd "$ISABELLE_HOME/src/Pure" >/dev/null |
101 pushd "$ISABELLE_HOME/src/Pure" >/dev/null |
102 "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!" |
102 "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!" |
103 popd >/dev/null |
103 popd >/dev/null |
104 |
|
105 if [ -d "$HOME/lib/jedit/current" ]; then |
|
106 pushd "$ISABELLE_HOME/lib/jedit/plugin" >/dev/null |
|
107 ./mk |
|
108 [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!" |
|
109 popd >/dev/null |
|
110 else |
|
111 echo "Warning: skipping jedit plugin" |
|
112 fi |
|
113 } |
104 } |
114 |
105 |
115 |
106 |
116 ## main |
107 ## main |
117 |
108 |