diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -12,6 +12,10 @@ $(delegated):: make -C $$i $@; \ done +# 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:: @ echo "Collecting traces" @ ./collect-traces.sh |
