diff options
Diffstat (limited to '_tags')
| -rw-r--r-- | _tags | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -79,5 +79,6 @@ "tools": include "tools/coqdoc": include "toplevel": include +"toplevel/utils": include <plugins/**>: include
\ No newline at end of file |