diff options
| -rw-r--r-- | .gitignore | 5 | ||||
| -rw-r--r-- | Makefile | 5 |
2 files changed, 4 insertions, 6 deletions
diff --git a/.gitignore b/.gitignore index 7dd8869b1..2b3e3aef1 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,2 @@ -*.o -*.hi -*.ho -*.a +build/* git-annex @@ -1,7 +1,8 @@ git-annex: - ghc --make git-annex + mkdir -p build + ghc -odir build -hidir build --make git-annex clean: - rm -f git-annex *.o *.hi *.ho *.a + rm -rf build git-annex .PHONY: git-annex |