Make it explicit when paths are added to the ML search paths.

When Mltop.add_rec_path was called to add paths to the loadpath, it was
also adding the top directory to the mlpath. In particular, "theories" was
added to the mlpath although it was explicitly marked "~with_ml:false".

The "plugins" and "user-contribs" subdirectories were scanned twice, once
for filling the loadpath and then for filling the mlpath.

This patch adds an argument to Mltop.add_rec_path to explicitly control
which paths from the loadpath are added to the mlpath (none, the top one,
all of them). The "top" option was the single old behavior; the "none"
option is used for "theories"; the "all" option is used to avoid
duplicate scanning for "plugins" and "user-contribs".

0 files changed, 0 insertions, 0 deletions