changeset 75230 | bbbee54b1198 |
parent 75220 | 1cbdf9cfc94b |
child 75273 | f1c6e778e412 |
--- a/src/Pure/General/path.scala Sun Mar 06 15:47:09 2022 +0100 +++ b/src/Pure/General/path.scala Sun Mar 06 17:45:47 2022 +0100 @@ -233,6 +233,7 @@ def tar: Path = ext("tar") def gz: Path = ext("gz") def log: Path = ext("log") + def orig: Path = ext("orig") def patch: Path = ext("patch") def backup: Path =