summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index dbae0f9..5395158 100644
--- a/Makefile
+++ b/Makefile
@@ -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