diff options
| author | Enrico Tassi | 2020-09-25 14:04:53 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:48 +0100 |
| commit | 4390b6907b3d07793c2e8f9e7ad3cc38d9488711 (patch) | |
| tree | 74a6d4eededf6f8ebb4119bdd9d1b15aa7de55b7 /vernac/vernac.mllib | |
| parent | 1fd4c22d493715f154f6b79dc7f6e4efd44ff185 (diff) | |
[vernac] move vernac_classifier to vernac
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
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 |