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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and