diff options
Diffstat (limited to 'egraph/retest.sh')
| -rwxr-xr-x | egraph/retest.sh | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/egraph/retest.sh b/egraph/retest.sh deleted file mode 100755 index c778fa1..0000000 --- a/egraph/retest.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -make clean && \ - make && \ - sudo make install && \ - make -C tests/ clean && \ - make -C tests/ run && \ - make -C examples clean && \ - make -C examples |