From 89e07c5a43c0637bc614b4396e6a8b3cb902cedb Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 6 Jan 2021 16:48:29 +1100 Subject: [PATCH] Get the Interaction-emacs manual built properly as part of release --- Manual/Interaction-emacs/.gitignore | 2 +- Manual/Interaction-emacs/Holmakefile | 10 +++++----- .../{HOL-interaction.stex => interaction-emacs.stex} | 0 developers/releasing-hol | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) rename Manual/Interaction-emacs/{HOL-interaction.stex => interaction-emacs.stex} (100%) diff --git a/Manual/Interaction-emacs/.gitignore b/Manual/Interaction-emacs/.gitignore index 3fbf11d918..57cb1cc05b 100644 --- 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 index 81324f0c65..161299d212 100644 --- 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/Manual/Interaction-emacs/HOL-interaction.stex b/Manual/Interaction-emacs/interaction-emacs.stex similarity index 100% rename from Manual/Interaction-emacs/HOL-interaction.stex rename to Manual/Interaction-emacs/interaction-emacs.stex diff --git a/developers/releasing-hol b/developers/releasing-hol index 6821757b61..b2c6503ab5 100755 --- 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"