Makefile: let make html depend on generated metrics.rst

.circleci/config.yml

@@ -64,7 +64,7 @@ jobs:
           name: Build docs to store
           command: |
             cd docs
-            make metrics html
+            make html
       # Tell Circle to store the documentation output in a folder that we can access later
       - store_artifacts:
           path: docs/build/html/

docs/Makefile

@@ -61,10 +61,12 @@ rest-api: source/_static/rest-api/index.html
 source/_static/rest-api/index.html: rest-api.yml node_modules
 	npm run rest-api
 
-metrics:
+metrics: source/monitoring/_gen/metrics.rst
+
+source/monitoring/_gen/metrics.rst: generate-metrics.py
 	python3 generate-metrics.py
 
-html: rest-api
+html: rest-api metrics
 	$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."

docs/generate-metrics.py

@@ -45,6 +45,7 @@ class Generator:
         content = f"{title}\n{underline}\n{writer.dumps()}"
         with open(filename, 'w') as f:
             f.write(content)
+        print(f"Generated {filename}.")
 
 
 def main():

docs/source/conf.py

@@ -217,7 +217,7 @@ intersphinx_mapping = {'https://docs.python.org/3/': None}
 on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
 if on_rtd:
     # readthedocs.org uses their theme by default, so no need to specify it
-    # build rest-api, since RTD doesn't run make
+    # build both metrics and rest-api, since RTD doesn't run make
     from subprocess import check_call as sh
 
     sh(['make', 'metrics', 'rest-api'], cwd=docs)