equal
deleted
inserted
replaced
470 """) |
470 """) |
471 |
471 |
472 |
472 |
473 /* diff */ |
473 /* diff */ |
474 |
474 |
475 Isabelle_System.bash( |
475 Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched)) |
476 "diff -ru " + Bash.string(jedit) + " " + Bash.string(jedit_patched) + |
|
477 " > " + Bash.string(jedit + ".patch"), |
|
478 cwd = component_dir.file).check_rc(_ <= 1) |
|
479 |
476 |
480 if (!original) Isabelle_System.rm_tree(jedit_dir) |
477 if (!original) Isabelle_System.rm_tree(jedit_dir) |
481 |
478 |
482 |
479 |
483 /* settings */ |
480 /* settings */ |