diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile b/Makefile index 5d8ed82..9aefa3e 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,7 @@ -all clean: +all clean check: @make -C src $@ @make -C minic $@ -check: all - test/go.sh all + sync-papers: unison -auto papers ssh://qcar@h/data/d/ssa-doc |