edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 10:41:08 +03:00
Code Issues Projects Releases Wiki Activity

[ admin ] add empty default target distinct from clean

Browse Source 
Tired of having to rebuild everything because I typed `make` in
the wrong directory.
This commit is contained in:
Guillaume Allais 2020-04-02 22:21:40 +01:00
parent 59503712f3
commit d92a65c43e
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Makefile
View File

@ -1,3 +1,5 @@
all:
clean:
rm -f YafflePaths.idr
find . -name '*.ibc' | xargs rm -f