src/Tools/jEdit/lib/Tools/jedit
changeset 53578 838d9e058a1a
parent 53577 d033bc00b762
child 53772 30de372ca56f
equal deleted inserted replaced
53577:d033bc00b762 53578:838d9e058a1a
   285       print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
   285       print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
   286     print; }' dist/modes/catalog
   286     print; }' dist/modes/catalog
   287 
   287 
   288   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   288   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   289   (
   289   (
   290     #workaround for scalac
   290     #workaround for scalac 2.10.2
   291     function stty() { :; }
   291     function stty() { :; }
   292     export -f stty
   292     export -f stty
   293 
   293 
   294     for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
   294     for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
   295     do
   295     do