diff options
| author | Jim Fehrle | 2020-08-09 14:25:51 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-24 15:38:33 -0700 |
| commit | 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a (patch) | |
| tree | ca46515653025f319db542241a30f8d58bbeeea3 /doc/sphinx/conf.py | |
| parent | 703d2c9a1ea576abb4f6f9abafb3f2e47aeac817 (diff) | |
Convert misc chapters to prodn
Diffstat (limited to 'doc/sphinx/conf.py')
| -rwxr-xr-x | doc/sphinx/conf.py | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index a8a574c861..75ac2a76cd 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,9 +183,7 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'collection', 'tactic', - 'bindings', 'induction_clause', 'conversion', 'where', |