equal
deleted
inserted
replaced
84 cp -R jars/. "$JEDIT/jars/." |
84 cp -R jars/. "$JEDIT/jars/." |
85 |
85 |
86 cp -R "$THIS/dist-template/." "$JEDIT/." |
86 cp -R "$THIS/dist-template/." "$JEDIT/." |
87 |
87 |
88 perl -i -e 'while (<>) { if (m/NAME="javacc"/) { |
88 perl -i -e 'while (<>) { if (m/NAME="javacc"/) { |
89 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,; |
|
90 print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.info"/>\n\n,; } |
90 print; }' "$JEDIT/modes/catalog" |
91 print; }' "$JEDIT/modes/catalog" |
91 |
92 |
92 |
93 |
93 # build archive |
94 # build archive |
94 |
95 |