Tutorial: mention shared repository management.

diff --git a/Makefile b/Makefile
index 88b89f956fc46e2e2b417efee654b48d7b12768f..3395a9e102957b02bbc6e1c25c56c8a97b8e5c76 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -397,6 +397,9 @@ $(patsubst %.py,%,$(SCRIPT_PYTHON)) : % : %.py
 git-cherry-pick: git-revert
        cp $< $@
 
+# format-patch records GIT_VERSION
+git-format-patch: Makefile
+
 %.o: %.c
        $(CC) -o $*.o -c $(ALL_CFLAGS) $<
 %.o: %.S