diff -r abd4a0f48e49 -r 28ac56e59d23 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Fri Jan 20 21:52:29 2023 +0100 +++ b/src/Pure/General/path.scala Fri Jan 20 21:56:34 2023 +0100 @@ -233,8 +233,12 @@ prfx + Path.basic(s + "." + e) } + def bib: Path = ext("bib") + def blg: Path = ext("blg") + def db: Path = ext("db") def gz: Path = ext("gz") def html: Path = ext("html") + def jar: Path = ext("jar") def log: Path = ext("log") def orig: Path = ext("orig") def patch: Path = ext("patch")