diff options
| author | Gaëtan Gilbert | 2019-05-07 14:56:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-07 14:57:13 +0200 |
| commit | 86fa401ceaa17bdf1d297808eff3f8c3792d2778 (patch) | |
| tree | ff6a2903a7faeef04c7e8292225b51c70ee3c02a /kernel/nativelambda.ml | |
| parent | 403f8784706d54e5e91bf20e56b0bf8ea40f4df3 (diff) | |
Fix PLUGINSVO computation after ltac2 integration
Avoid looking at random installed packages in -local mode.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions