# HG changeset patch
# User wenzelm
# Date 1456587426 -3600
# Node ID 183c319b26dc19fd3aab83c820971118332d6545
# Parent  fbccea37091d9b2e31c0b1c49d6c31a0443e692b
tuned messages;

diff -r fbccea37091d -r 183c319b26dc src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Sat Feb 27 16:19:02 2016 +0100
+++ b/src/Pure/System/getopts.scala	Sat Feb 27 16:37:06 2016 +0100
@@ -37,6 +37,7 @@
   private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
   private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
   private def option(opt: Char, opt_arg: List[Char]): Unit = options(opt)._2.apply(opt_arg.mkString)
+  private def print_option(opt: Char): String = quote("-" + opt.toString)
 
   private def getopts(args: List[List[Char]]): List[List[Char]] =
     args match {
@@ -50,10 +51,10 @@
       case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
         option(opt, opt_arg); getopts(rest_args)
       case List(List('-', opt)) if is_option1(opt) =>
-        Output.error_message("Command-line option " + quote(opt.toString) + " requires an argument")
+        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
         usage()
       case ('-' :: opt :: _) :: _ if !is_option(opt) =>
-        Output.error_message("Illegal command-line option " + quote(opt.toString))
+        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
         usage()
       case _ => args
   }