# HG changeset patch
# User wenzelm
# Date 1626254426 -7200
# Node ID c1277bb04507501db2e3cefb26c995fbc2edd1ab
# Parent  2d8a0f8e30ec76fc6df426cf9f3def83592b2e21
tuned;

diff -r 2d8a0f8e30ec -r c1277bb04507 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)