From 492fc8554da72738f485c859ab8336d2b2af9dd1 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 08:33:32 +0000 Subject: [PATCH 01/15] Branching make-mmref.py from mmref project to MPS so that we can validate Memory Management Reference builds from there. Copied from Perforce Change: 199111 --- manual/make-mmref.py | 190 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100755 manual/make-mmref.py diff --git a/manual/make-mmref.py b/manual/make-mmref.py new file mode 100755 index 0000000000..2046be0cd5 --- /dev/null +++ b/manual/make-mmref.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +# +# MAKE THE MEMORY MANAGEMENT REFERENCE +# Gareth Rees, Ravenbrook Limited, 2014-05-23 +# +# $Id$ +# +# +# 1. INTRODUCTION +# +# This script builds the Memory Management Reference website from the +# Memory Pool System manual. +# +# The whole build procedure is as follows: +# +# 1. Sync //info.ravenbrook.com/project/mps/master/manual/... +# 2. make html MMREF=1 +# 3. Run this script +# +# +# 2. DESIGN +# +# We build the Memory Management Reference out of the Memory Pool +# System manual because: +# +# 1. having a single set of sources makes it easier to work on; +# 2. the glossary is a vital tool in organizing the MPS manual; +# 3. cross-references from the MMRef to the MPS are an opportunity +# for advertising the latter to readers of the former. +# +# +# 3. DEPENDENCIES +# +# html5lib +# six + +import os +import re +from shutil import copyfile +import sys +from urllib.parse import urljoin +from xml.etree.cElementTree import Element + +import html5lib + + +# 4. CONFIGURATION + +# Subdirectories of the MPS manual that belong in the MMRef. +MMREF_DIRS = 'glossary mmref _images _static'.split() + +# Top-level files that belong in the MMRef. +MMREF_FILES = dict(index='mmref-index', bib='bib', copyright='mmref-copyright') + +# Regular expression matching files to be included in the MMRef. +URL_FILTER_RE = re.compile(r'/html/(?:(?:{})\.html)?(?:#.*)?$|/(?:{})/'.format( + '|'.join(MMREF_FILES), '|'.join(MMREF_DIRS))) + +# Root URL for the MPS manual. +REWRITE_URL = 'https://www.ravenbrook.com/project/mps/master/manual/html/' + + +def rewrite_links(src, src_base, url_filter, rewrite_base, + url_attributes=(('a', 'href'),)): + """Rewrite URLs and anchors in src and return the result. + + First, src is parsed as HTML. Second, all URLs found in the + document are resolved relative to src_base and the result passed + to the functions url_filter. If this returns False, the URL is + resolved again, this time relative to rewrite_base, and the result + stored back to the document. Third, all DT elements with an id + starting "term-X" are rewritten to contain another anchor with id + "X" (for backwards compatiblity with links to the old manual). + Finally, the updated document is serialized as HTML and returned. + + The keyword argument url_attributes is a sequence of (tag, + attribute) pairs that contain URLs to be rewritten. + + """ + tree = html5lib.parse(src, treebuilder='etree') + + for tag, attr in url_attributes: + for e in tree.iter('{http://www.w3.org/1999/xhtml}' + tag): + u = e.get(attr) + if u and not url_filter(urljoin(src_base, u)): + rewritten = urljoin(rewrite_base, u) + if u != rewritten: + e.set(attr, rewritten) + + id_re = re.compile(r'-([a-z])') + for dt in tree.iter('{http://www.w3.org/1999/xhtml}dt'): + id = dt.get('id') + if id and id.startswith('term-'): + span = Element('span', id=id_re.sub(r'.\1', id[5:])) + span.text = dt.text + dt.text = '' + for child in list(dt): + dt.remove(child) + span.append(child) + dt.insert(0, span) + + tree_walker = html5lib.getTreeWalker('etree') + html_serializer = html5lib.serializer.HTMLSerializer() + return u''.join(html_serializer.serialize(tree_walker(tree))) + + +def newer(src, target): + """Return True if src is newer (that is, modified more recently) than + target, False otherwise. + + """ + return (not os.path.isfile(target) + or os.path.getmtime(target) < os.path.getmtime(src) + or os.path.getmtime(target) < os.path.getmtime(__file__)) + + +def rewrite_file(src_dir, rel_dir, src_filename, target_path, rewrite_url): + src_path = os.path.join(src_dir, src_filename) + if not newer(src_path, target_path): + return + print("Rewriting links in {} -> {}".format(src_path, target_path)) + with open(src_path) as file: + src = file.read() + src_base = '/{}/'.format(src_dir) + url_filter = URL_FILTER_RE.search + rewrite_base = urljoin(rewrite_url, rel_dir + '/') + result = rewrite_links(src, src_base, url_filter, rewrite_base) + with open(target_path, 'w') as file: + file.write(result) + + +def main(src_root='html', target_root='mmref'): + for directory in MMREF_DIRS: + src_dir = os.path.join(src_root, directory) + target_dir = os.path.join(target_root, directory) + os.makedirs(target_dir, exist_ok=True) + for filename in os.listdir(src_dir): + src_path = os.path.join(src_dir, filename) + target_path = os.path.join(target_dir, filename) + if filename.endswith('.html'): + rewrite_file(src_dir, directory, filename, target_path, + REWRITE_URL) + elif os.path.isfile(src_path): + copyfile(src_path, target_path) + for target, src in MMREF_FILES.items(): + rewrite_file(src_root, '', '{}.html'.format(src), + os.path.join(target_root, '{}.html'.format(target)), + REWRITE_URL) + + +if __name__ == '__main__': + main(*sys.argv[1:]) + + +# B. DOCUMENT HISTORY +# +# 2014-05-23 GDR Created. +# 2018-10-29 GDR Port to Python 3 and html5lib 0.9999999. +# +# +# C. COPYRIGHT AND LICENCE +# +# Copyright (c) 2014-2018 Ravenbrook Ltd. All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are +# met: +# +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the +# distribution. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR +# CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# +# $Id$ From fd7dee66c12872a6cf37dabb22814fa6a82a628a Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 08:35:34 +0000 Subject: [PATCH 02/15] Incorporating the Memory Management Reference build target from //info.ravenbrook.com/project/mmref/master --- manual/.gitignore | 1 + manual/Makefile | 12 ++++++++++-- manual/requirements.pip | 4 ++++ 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/manual/.gitignore b/manual/.gitignore index f2a531e43c..5a17543431 100644 --- a/manual/.gitignore +++ b/manual/.gitignore @@ -2,6 +2,7 @@ doctrees converted epub html +mmref.in mmref source/design/*.rst source/design/*.svg diff --git a/manual/Makefile b/manual/Makefile index 25615b8571..f739874811 100644 --- a/manual/Makefile +++ b/manual/Makefile @@ -18,7 +18,7 @@ ALLSPHINXOPTS = -T -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) # the i18n builder cannot share the environment and doctrees with the others I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) source -.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest gettext +.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest gettext mmref help: @echo "Please use \`make ' where is one of" @@ -41,10 +41,11 @@ help: @echo " changes to make an overview of all changed/added/deprecated items" @echo " linkcheck to check all external links for integrity" @echo " doctest to run all doctests embedded in the documentation (if enabled)" + @echo " mmref to make the Memory Management Reference" @echo " tools to install a local copy of the Python tools using virtualenv" clean: - -for dir in changes devhelp dirhtml doctest doctrees epub html htmlhelp json latex linkcheck locale man pickle qthelp singlehtml texinfo text; do rm -rf $(BUILDDIR)/$$dir; done + -for dir in changes devhelp dirhtml doctest doctrees epub html htmlhelp json latex linkcheck locale man pickle qthelp singlehtml texinfo text mmref.in mmref; do rm -rf $(BUILDDIR)/$$dir; done -find $(BUILDDIR)/source/design -name '*.rst' ! -name 'index.rst' ! -name 'old.rst' -exec rm -f '{}' ';' html: $(SPHINXBUILD) @@ -158,6 +159,13 @@ doctest: $(SPHINXBUILD) @echo "Testing of doctests in the sources finished, look at the " \ "results in $(BUILDDIR)/doctest/output.txt." +.PHONY: mmref +mmref: $(SPHINXBUILD) + MMREF=1 $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/mmref.in + tool/bin/$(PYTHON) ./make-mmref.py $(BUILDDIR)/mmref.in $(BUILDDIR)/mmref + @echo + @echo "Build finished. The Memory Management Reference is $(BUILDDIR)/mmref." + .PHONY: tools tools: tool/bin/pip requirements.pip tool/bin/pip install -r requirements.pip diff --git a/manual/requirements.pip b/manual/requirements.pip index f5e50bda3e..d22bb939d9 100644 --- a/manual/requirements.pip +++ b/manual/requirements.pip @@ -2,3 +2,7 @@ # Layout breaks in Sphinx >= 5. See . sphinx >= 4, < 5 + +# HTML parser based on the WHATWG HTML specification +# Required by make-mmref.py +html5lib From 4146715a1253a9ba7dcb8e528997545d52bb7ab2 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 19:31:17 +0000 Subject: [PATCH 03/15] Add post-processing to build the Memory Management Reference. --- .readthedocs.yaml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 8ae20323cd..bdb6005d78 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -19,6 +19,21 @@ build: os: ubuntu-22.04 tools: python: '3' + jobs: + # If MMREF is set then this config is being run to build the + # Memory Management Reference, which requires post-processing by + # the make-mmref.py script. + # + # FIXME: Duplicates code in manual/Makefile in a hacky way, but + # simply calling that Makefile would disable various Read the Docs + # features. + # + # See . + post_build: + - if test -n "${MMREF}"; then \ + mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && \ + python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html" \ + fi python: install: @@ -37,6 +52,7 @@ sphinx: # B. DOCUMENT HISTORY # # 2023-02-02 RB Created as part of MPS GitHub migration. +# 2023-03-03 RB Updated to also build the Memory Management Reference. # # # C. COPYRIGHT AND LICENSE From 9fbc6224dbe1b645568fd32a938c77f84ef67d3a Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 19:35:42 +0000 Subject: [PATCH 04/15] Correcting YAML syntax of post_build script. --- .readthedocs.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index bdb6005d78..1fd00c8b55 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,9 +30,9 @@ build: # # See . post_build: - - if test -n "${MMREF}"; then \ - mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && \ - python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html" \ + - if test -n "${MMREF}"; then + mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && + python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html" fi python: From 2a642594a525a3cbcd0d9c10f686bf6b6e43307c Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 19:40:06 +0000 Subject: [PATCH 05/15] Another attempt to correct the post_build script. --- .readthedocs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 1fd00c8b55..b118b27ab5 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -32,7 +32,7 @@ build: post_build: - if test -n "${MMREF}"; then mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && - python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html" + python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; fi python: From 7fdbbd3ff01544484ba5a518b46c96dc9c98f1f3 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 3 Mar 2023 19:47:22 +0000 Subject: [PATCH 06/15] Yet another attempt to fix the post_build script, using a literal scalar. --- .readthedocs.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index b118b27ab5..25e0ae583b 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,8 @@ build: # # See . post_build: - - if test -n "${MMREF}"; then + - | + if test -n "${MMREF}"; then mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; fi From 82f0d180a1bb0a7909d94eee22ab4a7b71a7dea3 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:37:36 +0000 Subject: [PATCH 07/15] Trying to overcome mysterious shell errors on Read the Docs that I can't reproduce locally. --- .readthedocs.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 25e0ae583b..0da107a2b6 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -31,7 +31,8 @@ build: # See . post_build: - | - if test -n "${MMREF}"; then + if test -n "${MMREF}"; + then mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; fi From b3a28a6cc3bb410523bb28cdcb8b4f28fedd4ac6 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:40:17 +0000 Subject: [PATCH 08/15] Another attempt to overcome weird shell errors. --- .readthedocs.yaml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 0da107a2b6..431d00748b 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -31,11 +31,12 @@ build: # See . post_build: - | - if test -n "${MMREF}"; - then - mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && - python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; - fi + sh -c ' + if test -n "${MMREF}"; then + mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && + python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; + fi + ' python: install: From 044e790f24217ad709dbc8ced9c35febaf02f0e9 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:43:24 +0000 Subject: [PATCH 09/15] One more try. --- .readthedocs.yaml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 431d00748b..6b2f5c7a59 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,13 +30,7 @@ build: # # See . post_build: - - | - sh -c ' - if test -n "${MMREF}"; then - mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && - python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; - fi - ' + - if test -n "${MMREF}"; then mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; fi python: install: From 4a07b8418a4e5b1036dd50f13552098308972fb2 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:46:47 +0000 Subject: [PATCH 10/15] Testing Read the Docs post_build shell --- .readthedocs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 6b2f5c7a59..7aebab072d 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,7 @@ build: # # See . post_build: - - if test -n "${MMREF}"; then mv "${READTHEDOCS_OUTPUT}/html" "${READTHEDOCS_OUTPUT}/mmref.in" && python manual/make-mmref.py "${READTHEDOCS_OUTPUT}/mmref.in" "${READTHEDOCS_OUTPUT}/html"; fi + - echo A B C D; echo E F G H python: install: From 1106c9cd066c9638ccf2f7772083384bb526673f Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:49:38 +0000 Subject: [PATCH 11/15] Testing the Read the Docs shell. --- .readthedocs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 7aebab072d..d6ef73dbaa 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,7 @@ build: # # See . post_build: - - echo A B C D; echo E F G H + - if test -n "A"; then echo "B"; fi python: install: From 751f19cc4d59e126a487b264055e1051039f5b39 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 04:52:59 +0000 Subject: [PATCH 12/15] Debugging the Read the Docs shell. --- .readthedocs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index d6ef73dbaa..48cfcb4113 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,7 @@ build: # # See . post_build: - - if test -n "A"; then echo "B"; fi + - if [ "A" = "A" ]; then echo "B"; fi python: install: From c41ce2b109f62038402920f341fc1d886f87f27e Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 05:10:34 +0000 Subject: [PATCH 13/15] Is it quoting? --- .readthedocs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 48cfcb4113..7407f28eb9 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,7 @@ build: # # See . post_build: - - if [ "A" = "A" ]; then echo "B"; fi + - if [ 'A' = 'A' ]; then echo 'B'; fi python: install: From b08bcf32bcd8d0e38e3e4bcc474820c16eda53e6 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 05:26:45 +0000 Subject: [PATCH 14/15] Try literal copy of Read the Docs example. --- .readthedocs.yaml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 7407f28eb9..b21d213c1d 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -30,7 +30,11 @@ build: # # See . post_build: - - if [ 'A' = 'A' ]; then echo 'B'; fi + - | + if [ "$READTHEDOCS_VERSION_TYPE" = "external" ] && git diff --quiet origin/main -- docs/ .readthedocs.yaml; + then + exit 183; + fi python: install: From 6133148eb91b8425cad68b6dfe5544c00e736f69 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 4 Mar 2023 05:41:46 +0000 Subject: [PATCH 15/15] Try overring the entire build. --- .readthedocs.yaml | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index b21d213c1d..abfb78973a 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -19,22 +19,16 @@ build: os: ubuntu-22.04 tools: python: '3' - jobs: - # If MMREF is set then this config is being run to build the - # Memory Management Reference, which requires post-processing by - # the make-mmref.py script. - # - # FIXME: Duplicates code in manual/Makefile in a hacky way, but - # simply calling that Makefile would disable various Read the Docs - # features. - # - # See . - post_build: - - | - if [ "$READTHEDOCS_VERSION_TYPE" = "external" ] && git diff --quiet origin/main -- docs/ .readthedocs.yaml; - then - exit 183; - fi + # Override the Read the Docs build with our own. This uses a beta + # feature of Read the Docs that loses some features + # + # but attempts at using post_build to do post-processing have so far + # failed + # . + commands: + - make -C manual html mmref + - mkdir -p _readthedocs + - if test -n "$MMREF"; then mv manual/mmref _readthedocs/html; else mv manual/html _readthedocs/html; fi python: install: