lib/Tools/setup
changeset 73745 d31d229eb8df
parent 73744 9460f1f45405
child 73746 dbe5bbc2331e
equal deleted inserted replaced
73744:9460f1f45405 73745:d31d229eb8df
    98     PULL=""
    98     PULL=""
    99   else
    99   else
   100     PULL=true
   100     PULL=true
   101   fi
   101   fi
   102 
   102 
   103   isabelle components -I
   103   isabelle components -I || exit "$?"
   104 
   104 
   105   #Atomic exec: avoid inplace update of running script!
   105   #Atomic exec: avoid inplace update of running script!
   106   export CLEAN PULL
   106   export CLEAN PULL
   107   exec bash -c '
   107   exec bash -c '
   108     set -e
   108     set -e