[isabelle-dev] Silent exit if settings file has non-zero exit code

[Makarius]

On Fri, 11 Feb 2011, Lars Noschinski wrote:

> I just noticed that the main isabelle executable exits silently if the 
> last command in a settings file has a non-zero exit code (this might 
> happen quite naturally if for example $PATH_OF_COMPONENT does not exist 
> in the following construct:
>
>   [ -d "$PATH_OF_COMPONENT" ] && init_component "$PATH_OF_COMPONENT"

I am using this form myself quite often, but did not notice this effect 
yet, since my settings are even more complex.

See now http://isabelle.in.tum.de/repos/isabelle/rev/bf49b7a85936 which 
attempts to make this situation less surprising, without 
overinterpretation of error situtations by pretending to be smart.


> Is this intentional or would a patch outputting an error message be 
> acceptable?

Such questions can only be answered from the history of the sources, in 
particular 
http://isabelle.in.tum.de/repos/isabelle/log/bf49b7a85936/lib/scripts/getsettings

It is quite interesting to follow the twisted path of the "exit 2" that is 
responsible for the above behaviour.  In the very beginning the sitation 
was much easier to oversee: 
http://isabelle.in.tum.de/repos/isabelle/file/ed9720047d53/lib/scripts/getsettings


 	Makarius