diff options
| author | Théo Zimmermann | 2020-06-05 13:05:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-05 13:36:58 +0200 |
| commit | 4f4ad5678db3e7aaf42f14d6d2d9000550c5f826 (patch) | |
| tree | 4bf0c6f1f89f2cd5b804b79bdb60022df73d9bfd | |
| parent | db768e6828af62e06eb03d36509be6f8fc1efbf3 (diff) | |
Fix version switcher when building with Dune.
Closes #12395.
| -rw-r--r-- | doc/sphinx/dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/dune b/doc/sphinx/dune index b788fbbeed..31f28635fe 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,4 +1,4 @@ -(dirs :standard _static) +(dirs :standard _static _templates) (rule (targets README.gen.rst) |