equal
deleted
inserted
replaced
78 |
78 |
79 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
79 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
80 cp -R "$JEDIT_HOME/." "$JEDIT/." |
80 cp -R "$JEDIT_HOME/." "$JEDIT/." |
81 rm -rf "$JEDIT/jEdit" "$JEDIT/build-support" |
81 rm -rf "$JEDIT/jEdit" "$JEDIT/build-support" |
82 |
82 |
83 cp -R jars "$JEDIT/jars" |
83 mkdir -p "$JEDIT/jars" |
|
84 cp -R jars/. "$JEDIT/jars/." |
84 |
85 |
85 cp -R "$THIS/dist-template/." "$JEDIT/." |
86 cp -R "$THIS/dist-template/." "$JEDIT/." |
86 |
87 |
87 perl -i -e 'while (<>) { if (m/NAME="javacc"/) { |
88 perl -i -e 'while (<>) { if (m/NAME="javacc"/) { |
88 print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; } |
89 print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; } |