diff options
Diffstat (limited to 'script')
| -rwxr-xr-x | script/clean-up-dir.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/script/clean-up-dir.sh b/script/clean-up-dir.sh index fefb513230..0d517f0595 100755 --- a/script/clean-up-dir.sh +++ b/script/clean-up-dir.sh @@ -5,6 +5,8 @@ find . -name "*.plperl" -delete find . -name "*.ipynb" -delete find . -name "*.Mod" -delete find . -name "*.gp" -delete +find . -name "*.exs" -delete +find . -name "*.dws" -delete find . -name "*.v" -delete find . -name "*.fsx" -delete find . -name "*.tex" -delete |