From 4adb9cdf82b1d83d09586d7c6af9e507cc57cb4e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 17 Jan 2025 12:04:00 +0100
Subject: [PATCH] [scripts] git-replace.sh: Add script description

---
 bin/migration_scripts/git-replace.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/bin/migration_scripts/git-replace.sh b/bin/migration_scripts/git-replace.sh
index 7eac6e7917..0fb64f3b97 100755
--- a/bin/migration_scripts/git-replace.sh
+++ b/bin/migration_scripts/git-replace.sh
@@ -21,6 +21,9 @@
 #                                                                        #
 ##########################################################################
 
+# Patch old private git history to the new public git history.
+# (only useful on private frama-c/frama-c repository)
+
 git replace fbe13264f29d59b5388096281f98f05116b17f76 8e6afe71d01b1bc4f4d778a5326d0a2e1f2998b3
 git replace cef5bf08946dccaf6b51e515eea76443976e6550 8bd30e2d47ffab72507d5ea291bdbd9f0fea0384
 git replace dbdd833de897111300f4525844170643fa8b5986 38863fe7d7d53aaf9e31703b738170f743b0b172
-- 
GitLab