equal
deleted
inserted
replaced
1 #!/bin/csh |
1 #!/bin/csh |
2 # Executed from the main Isabelle directory, this script removes all files |
2 # Executed from the main Isabelle directory, this script removes all files |
3 # made when Isabelle was used with set MAKE_HTML |
3 # made when Isabelle was used with set MAKE_HTML |
4 |
4 |
5 rm */.theory_list.txt */index.html */.*.html */*/.*.html */*/*/.*.html |
5 rm */.theory_list.txt */*/.theory_list.txt */*/*/.theory_list.txt \ |
|
6 */index.html */*/index.html */*/*/index.html \ |
|
7 */.*.html */*/.*.html */*/*/.*.html |