Re: [isabelle] Presenting theories without running a session

On 13.02.2011 15:16, Makarius wrote:
On Thu, 10 Feb 2011, Robert Lamar wrote:
/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?

That is in bash. In my favored shell, zsh, the shell gives an error
because it thinks the ? is a wildcard.

It is a wildcard, so you will get strange effects if you've got a file named e.g. "-b" in your current directory ;)

I've seen this effect for the last time with tcsh, many many years ago.

I can reproduce this error message with bash 4.1.5(1); on a Debian system. This is a warning output by getopts, as "?" is not in the list of valid arguments (nor ":" is given as first element in the optstring, to enable silent error reporting).

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.