author | wenzelm |
Wed, 14 Jul 2021 11:20:26 +0200 | |
changeset 73982 | c1277bb04507 |
parent 73977 | 2d8a0f8e30ec |
child 73983 | e2913fc81142 |
--- a/src/Pure/Admin/build_jedit.scala Wed Jul 14 10:02:43 2021 +0200 +++ b/src/Pure/Admin/build_jedit.scala Wed Jul 14 11:20:26 2021 +0200 @@ -661,7 +661,7 @@ """, "D:" -> (arg => target_dir = Path.explode(arg)), "J:" -> (arg => java_home = Path.explode(arg)), - "O" -> (arg => original = true), + "O" -> (_ => original = true), "V:" -> (arg => version = arg)) val more_args = getopts(args)