From 4390b6907b3d07793c2e8f9e7ad3cc38d9488711 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 25 Sep 2020 14:04:53 +0200
Subject: [vernac] move vernac_classifier to vernac

---
 vernac/vernac.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/vernac.mllib')

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd0dd5e9a6..007a3b05fc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -45,3 +45,4 @@ ComArguments
 Vernacentries
 ComTactic
 Vernacinterp
+Vernac_classifier
-- 
cgit v1.2.3