docs: releases take a little bit longer now

nedbat · Dec 23, 2022 · c5cda3a · c5cda3a
1 parent 9d4226e
commit c5cda3a
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/howto.txt b/howto.txt
@@ -31,8 +31,11 @@
     - IF NOT PRE-RELEASE:
         $ make sample_html
         check in the new sample html
-- Done with changes to source files, check them in.
-    $ git push
+- Done with changes to source files
+    - check them in on a branch
+    - wait for ci to finish
+    - merge to master
+    - git push
 - Build and publish docs:
     - IF PRE-RELEASE:
         $ make publishbeta