diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rwxr-xr-x | build/run | 4 |
2 files changed, 1 insertions, 4 deletions
@@ -86,6 +86,7 @@ build/gprof.txt build/gprof.dot build/gmon.out build/out.txt +build/run # debian debian/* diff --git a/build/run b/build/run deleted file mode 100755 index 17c9955..0000000 --- a/build/run +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash - -../run/bin/mplint >out.txt - |