No need to add a new commit in the history for every new doc publish

yawaramin · Apr 27, 2024 · 8b7c862 · 8b7c862
1 parent 75fb2a1
commit 8b7c862
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -2,7 +2,7 @@ DOCPATH=$(PWD)/_build/default/_doc/_html
 
 .PHONY : publish_doc
 publish_doc : odoc
-	@git checkout gh-pages && cp -R $(DOCPATH)/* . && rm -rf dream_html && git add . && git commit -mdocs && git push --force && git checkout -
+	@git checkout gh-pages && cp -R $(DOCPATH)/* . && rm -rf dream_html && git add . && git commit --amend -mdocs && git push --force && git checkout -
 
 .PHONY : publish_opam
 publish_opam :