[ci skip] Add gotcha in howto_release

jump-dev · Feb 17, 2019 · ce1ac6d · ce1ac6d
1 parent 0fa6f12
commit ce1ac6d
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/howto_release.txt b/howto_release.txt
@@ -1,8 +1,12 @@
-This note serves as developer documentation for the JuMP release process, which has accumulated a number of manual steps.
+This note serves as developer documentation for the JuMP release process, which
+has accumulated a number of manual steps.
 
 Steps for a new major (0.xx) release:
 
 - Update NEWS.md
 - Create release-0.xx branch
 - Update version and branches in README.md
 - Check that CI passes on release branch
+
+/!\ When creating a tag, check that it is not created on a commit with
+    `[ci skip]`, see https://github.com/JuliaDocs/Documenter.jl/issues/965