diff options
author | Jonas Bernoulli <jonas@bernoul.li> | 2017-04-18 18:18:31 +0200 |
---|---|---|
committer | Clément Pit-Claudel <cpitclaudel@gmail.com> | 2017-04-18 14:17:09 -0400 |
commit | 28ee469c90b9673cce21c1ea4e34d5dc3406ad56 (patch) | |
tree | a22f60815e8acdb25b4c5767a3e0a9492c4de7ab /coq | |
parent | 91eecd79d875c56afb12a4064590be71eeff6721 (diff) |
Add file contrib/mmm/.nosearch to help feature extraction tools
This change is intended as an intermediate step toward the removal
of the bundled copy of `mmm' package. Even with this change, PG
continues to use the bundled version, unless `mmm-auto' is already
loaded at the time PG first loads `proof-auxmodes'.
The benefit of this change is that tools that extract the features
provided and required by a package, such as those used to maintain
the Emacsmirror, will no longer be tricked into believing that
`mmm' is part of PG.
Eventually the bundled `mmm' copy should be removed completely, as I
suggested in #171, and as was already on the roadmap before I did so.
Diffstat (limited to 'coq')
0 files changed, 0 insertions, 0 deletions