ztest-to-coding.sh
changeset 59320 4549c6062b30
parent 59316 3a60188d9cc3
child 59375 946735bfc15a
     1.1 --- a/ztest-to-coding.sh	Fri Nov 17 05:49:54 2017 +0100
     1.2 +++ b/ztest-to-coding.sh	Thu Jan 18 15:25:39 2018 +0100
     1.3 @@ -1,8 +1,10 @@
     1.4  # switches isac from test-mode to coding-mode:
     1.5 -# this closes signatures as much as possible for coding;
     1.6 +# this closes signatures as much as possible for coding.
     1.7  
     1.8  cd src/Tools/isac
     1.9  find . -type f -exec sed -i s/'--- ! aktivate for Test_Isac BEGIN ---\\\*)'/'--- ! aktivate for Test_Isac BEGIN ---\\\* )'/g {} \;
    1.10  find . -type f -exec sed -i s/'(\*\\--- ! aktivate for Test_Isac END ---'/'( \*\\--- ! aktivate for Test_Isac END ---'/g {} \;
    1.11 -cd ../../../
    1.12 -./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &
    1.13 \ No newline at end of file
    1.14 +cd ../../../  # go back to ~~/.
    1.15 +
    1.16 +# immediately go to correcting code in Interpret/
    1.17 +./bin/isabelle jedit src/Tools/isac/Interpret/Interpret.thy &