From c1aa2b4faefd8a81a3af01e846f607de1815818a Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 18 Apr 2025 11:25:18 +0900 Subject: [PATCH] updating README.md and Makefile --- Makefile | 15 ++++++++------- README.md | 16 +++++++++------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/Makefile b/Makefile index 0b363a93..ce9dedab 100644 --- a/Makefile +++ b/Makefile @@ -1,9 +1,10 @@ -# this +ORG_FILES=$(wildcard *.org) +HTML_FILES=$(ORG_FILES:.org=.html) -R=1.6 +# default target does nothing +all: -import-doc: - -git subtree add -P htmldoc release/$(R) - T=`git subtree split -P htmldoc release/$(R)`;\ - git subtree merge -P htmldoc --squash $$T \ - -m 'importing htmldoc from $(R)' +org-html: $(HTML_FILES) + +%.html: %.org + emacs --batch $< -e org-html-export-to-html diff --git a/README.md b/README.md index 05709e70..3012a2f3 100644 --- a/README.md +++ b/README.md @@ -14,17 +14,19 @@ Please push a git tag with every commit inserting a new reference, so that watchers get notified. ## Tips - + Html files pushed here are put online straight away. -Running `make` in the htmldoc directory updates the html files -generated by coqdoc and the library graph. +The steps to produce the updated documentation for `math-comp` are +reported on the [MathComp GitHub wiki](https://github.com/math-comp/math-comp/wiki/Howto-Release#steps) Some html files are actually generated from eponymous org files (extension `.org`). They are generated using emacs: open the `blah.org` with emacs, press `C-c C-e h h` to generate the -corresponding `blah.html`. After editing the `.org` file, you -should perform this operation to generate the `.html` file. Both files -can then be committed and pushed on the main repository (just modifying -the `org` file and pushing has no effect on the displayed page). +corresponding `blah.html`. Alternatively, run the command `make org-html` +from the main folder. After editing the `.org` file, you +should perform this operation to generate the `.html` file. Both +files can then be committed and pushed on the main repository (just +modifying the `org` file and pushing has no effect on the displayed +page).