diff -r 075467e070ba -r bbbee54b1198 src/Pure/General/path.scala --- 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 =