Re: [isabelle] Presenting theories without running a session
On Thu, 10 Feb 2011, Robert Lamar wrote:
As an aside, here is something I noticed about the behavior of the
isabelle command line tool. I can work around it, I am just sharing it
for your information as a possible bug: typing 'isabelle' at a command
prompt gives usage information, and includes the message 'pass "-?" for
tool specific help.' But if I type, say, 'isabelle usedir -?', it gives
the following message along with the expected usage info for usedir:
/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.
I've seen this effect for the last time with tcsh, many many years ago.
The usage message of the Isabelle scripts is correct in asking for "-?"
but it depends on the context how you need to produce that externally.
Here the context is prose English, so I have some quotes around it. Bash
will accept it without quotes. Other shells will have there own idea.
This archive was generated by a fusion of
Pipermail (Mailman edition) and