diff options
| author | Jonas Bernoulli | 2017-04-18 18:18:31 +0200 |
|---|---|---|
| committer | Clément Pit-Claudel | 2017-04-18 14:17:09 -0400 |
| commit | 28ee469c90b9673cce21c1ea4e34d5dc3406ad56 (patch) | |
| tree | a22f60815e8acdb25b4c5767a3e0a9492c4de7ab | |
| 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.
| -rw-r--r-- | contrib/mmm/.nosearch | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/contrib/mmm/.nosearch b/contrib/mmm/.nosearch new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/contrib/mmm/.nosearch |