| Sun, 13 Feb 2011 17:45:21 +0100 | wenzelm | more explicit exit due to failed etc/settings -- normally return code 0=true and 1=false could be tolerated, but bash syntax errors also return 1; | file | diff | annotate |
| Sun, 13 Feb 2011 17:29:44 +0100 | wenzelm | eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist; | file | diff | annotate |
| Sun, 13 Feb 2011 17:19:43 +0100 | wenzelm | tuned; | file | diff | annotate |