| changeset 73490 | d31d229eb8df |
| parent 73489 | 9460f1f45405 |
| child 73491 | dbe5bbc2331e |
| 73489:9460f1f45405 | 73490: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 |