diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -12,10 +12,15 @@ $(delegated):: make -C $$i $@; \ done +clean:: + - rm traces.tgz + # To generate complete traces, apply this patch before running "make traces": # $ git apply traces.patch # To update this patch, add print statements, then run # $ git diff src > traces.patch -traces:: +traces:: traces.tgz + +traces.tgz: @ echo "Collecting traces" @ ./collect-traces.sh |
