# 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)