From 6f95cb1f104759d198f252c3064ba061a52918c0 Mon Sep 17 00:00:00 2001
From: Kévin Le Gouguec <kevin.legouguec@airbus.com>
Date: Wed, 28 Nov 2018 14:56:20 +0100
Subject: Ajout de patchs pour la génération de traces
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

… Y a probablement une façon plus  simple de gérer tout ça, mais je la
vois pas là tout de suite.
---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile')

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
-- 
cgit v1.2.3