diff --git a/configure b/configure index 1986e666..98f5f1ea 100755 --- a/configure +++ b/configure @@ -1551,16 +1551,16 @@ NOTMUCH_HAVE_PYTHON3_PYTEST=${have_python3_pytest} PLATFORM=${platform} EOF -cat > sphinx.config <> sphinx.config -fi -if [ $WITH_PYTHON_DOCS = "1" ]; then - printf "tags.add('WITH_PYTHON')\n" >> sphinx.config -fi -printf "rsti_dir = '%s'\n" $(realpath emacs) >> sphinx.config +{ + echo "# Generated by configure, run from doc/conf.py" + if [ $WITH_EMACS = "1" ]; then + echo "tags.add('WITH_EMACS')" + fi + if [ $WITH_PYTHON_DOCS = "1" ]; then + echo "tags.add('WITH_PYTHON')" + fi + printf "rsti_dir = '%s'\n" $(realpath emacs) +} > sphinx.config # Finally, after everything configured, inform the user how to continue. cat <