From 90285ff50290a49d20d60ffc59725bf87c6acd14 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 1 May 2020 13:22:42 +0200
Subject: Move essential vocabulary and syntax conventions to section on
 basics.

---
 doc/sphinx/conf.py | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx/conf.py')

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index db1340eacb..dbe582df95 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -186,6 +186,7 @@ nitpick_ignore = [ ('token', token) for token in [
     'binders',
     'collection',
     'modpath',
+    'tactic',
 ]]
 
 # -- Options for HTML output ----------------------------------------------
-- 
cgit v1.2.3