Get the Interaction-emacs manual built properly as part of release

HOL-Theorem-Prover · Jan 6, 2021 · 89e07c5 · 89e07c5
1 parent 18e3529
commit 89e07c5
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/Manual/Interaction-emacs/.gitignore b/Manual/Interaction-emacs/.gitignore
@@ -1 +1 @@
-HOL-interaction.tex
+interaction-emacs.tex
diff --git a/Manual/Interaction-emacs/Holmakefile b/Manual/Interaction-emacs/Holmakefile
@@ -2,13 +2,13 @@ INCLUDES = $(HOLDIR)/Manual/Tools
 
 SCRIPTER = $(HOLDIR)/Manual/Tools/polyscripter
 
-all: HOL-interaction.pdf
+all: interaction-emacs.pdf
 .PHONY: all
 
-HOL-interaction.pdf: HOL-interaction.tex
-	latexmk -pdf HOL-interaction
+interaction-emacs.pdf: interaction-emacs.tex
+	latexmk -pdf interaction-emacs
 
-HOL-interaction.tex: HOL-interaction.stex $(dprot $(SCRIPTER))
+interaction-emacs.tex: interaction-emacs.stex $(dprot $(SCRIPTER))
 	$(protect $(SCRIPTER)) $(protect $(HOLDIR)/Manual/Tools/umap) < $< > $@
 
-EXTRA_CLEANS = $(patsubst %,HOL-interaction.%,aux fdb_latexmk fls log pdf tex)
+EXTRA_CLEANS = $(patsubst %,interaction-emacs.%,aux fdb_latexmk fls log pdf tex)
diff --git a/...al/Interaction-emacs/HOL-interaction.stex → .../Interaction-emacs/interaction-emacs.stex b/...al/Interaction-emacs/HOL-interaction.stex → .../Interaction-emacs/interaction-emacs.stex
diff --git a/developers/releasing-hol b/developers/releasing-hol
@@ -177,7 +177,7 @@ else
 fi
 
 echo ; echo Building documentation
-for man_name in Reference Description Tutorial Quick Logic Developers
+for man_name in Description Developers Interaction-emacs Logic Quick Reference Tutorial
 do
     lcname=$(echo $man_name | tr A-Z a-z)
     echo -n "  $man_name"