From eeec78f9f9fd8ed26d4f42b0d5ea7d12a2910321 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Mon, 9 Jan 2023 14:30:12 +0100
Subject: [PATCH] avoid leaving the git repository in a detached state

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e33c6ff..5a636a6 100644
--- a/README.md
+++ b/README.md
@@ -62,9 +62,10 @@ révision, il faut effectuer les opérations suivantes:
 git checkout main
 cp make_single_short.pl tmp.pl
 ./make_single_short.pl > expanded_short.tex
-git checkout e92dfdf9
+git checkout e92dfdf9 # choose you own revision identifier here
 ./tmp.pl > old_expanded_short.tex
 latexdiff old_expanded_short.tex expanded_short.tex > pre_diff.tex
 sed -e "/DIF/s/.url//" pre_diff.tex > diff.tex
 pdflatex diff
+git checkout main
 ```
-- 
GitLab