Skip to content

Commit 17e4fb9

Browse files
committed
End the reign of terror of README.template.rst
doc/sphinx/README.rst is no longer generated. No more diff between README.gen.rst No more python script regen_readme.py No more README.template.rst
1 parent e755695 commit 17e4fb9

File tree

4 files changed

+1
-398
lines changed

4 files changed

+1
-398
lines changed

doc/sphinx/README.template.rst

Lines changed: 0 additions & 321 deletions
This file was deleted.

doc/sphinx/conf.py

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -146,9 +146,7 @@ def setup(app):
146146
'.DS_Store',
147147
'introduction.rst',
148148
'refman-preamble.rst',
149-
'README.rst',
150-
'README.gen.rst',
151-
'README.template.rst'
149+
'README.rst'
152150
] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS]
153151

154152
# The reST default role (used for this markup: `text`) to use for all

doc/sphinx/dune

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1 @@
11
(dirs :standard _static _templates)
2-
3-
(rule
4-
(targets README.gen.rst)
5-
(deps (source_tree ../tools/coqrst) README.template.rst)
6-
(action (run ../tools/coqrst/regen_readme.py %{targets})))
7-
8-
(rule
9-
(alias refman-html)
10-
(action (diff README.rst README.gen.rst)))

0 commit comments

Comments
 (0)