eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;
authorwenzelm
Sun Feb 13 17:29:44 2011 +0100 (2011-02-13)
changeset 417596aa5804aaf90
parent 41758 a231e6110f9b
child 41760 bf49b7a85936
eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Sun Feb 13 17:19:43 2011 +0100
     1.2 +++ b/lib/scripts/getsettings	Sun Feb 13 17:29:44 2011 +0100
     1.3 @@ -152,9 +152,6 @@
     1.4  
     1.5  #main components
     1.6  init_component "$ISABELLE_HOME"
     1.7 -
     1.8 -[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
     1.9 -  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
    1.10  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
    1.11  
    1.12  #ML system identifier