equal
deleted
inserted
replaced
467 if (!original) Isabelle_System.rm_tree(jedit_dir) |
467 if (!original) Isabelle_System.rm_tree(jedit_dir) |
468 |
468 |
469 |
469 |
470 /* settings */ |
470 /* settings */ |
471 |
471 |
472 File.write(component_dir.settings, |
472 component_dir.write_settings(""" |
473 """# -*- shell-script -*- :mode=shellscript: |
|
474 |
|
475 JEDIT_HOME="$COMPONENT/""" + jedit_patched + """" |
473 JEDIT_HOME="$COMPONENT/""" + jedit_patched + """" |
476 JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """ |
474 JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """ |
477 JEDIT_JAR="$JEDIT_HOME/jedit.jar" |
475 JEDIT_JAR="$JEDIT_HOME/jedit.jar" |
478 classpath "$JEDIT_JAR" |
476 classpath "$JEDIT_JAR" |
479 |
477 |