Re: [isabelle] Presenting theories without running a session



On Mon, Feb 14, 2011 at 9:17 AM, Lars Noschinski <noschinl at in.tum.de> wrote:
> 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 ;)

Indeed!  I was merely suggesting that it would be *even better* to use
a character that is not a wildcard.  :c)  I propos '-h', as it does
not seem to be used as an option by any of the tools.
>
>> 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).

Very interesting.  I had not dug quite that deeply.  It looks to me
that appending '\?' to the lists of getopts options (for instance,
line 93 in lib/Tools/usedir) would make the error go away.  Can you
see any problem with this?

-- 
Robert





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