diff --git a/distrib/core/HOWTO b/distrib/core/HOWTO
index b54b5dc1798b7055365a9f1f2c48c04c5067b559..38716f09fd2a4e427134a8cf6b358cd86cae221b 100755
--- a/distrib/core/HOWTO
+++ b/distrib/core/HOWTO
@@ -4,6 +4,7 @@ cd /G/f2
 git checkout master
 git pull origin master
 git merge devel
+git rebase -i HEAD~99 # correct commit messages; merge correction commits
 git push origin master
 
 ### prepare