tuned;
authorwenzelm
Wed, 14 Jul 2021 11:20:26 +0200
changeset 73982 c1277bb04507
parent 73977 2d8a0f8e30ec
child 73983 e2913fc81142
tuned;
src/Pure/Admin/build_jedit.scala
--- 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)