diff options
Diffstat (limited to 'src/nbc/clean.sh')
| -rw-r--r-- | src/nbc/clean.sh | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/nbc/clean.sh b/src/nbc/clean.sh deleted file mode 100644 index 58d95bf..0000000 --- a/src/nbc/clean.sh +++ /dev/null @@ -1,2 +0,0 @@ -#! /bin/sh -v -rm substitution.lex.sml substitution.grm.sig substitution.grm.sml score |