diff options
Diffstat (limited to 'api_docgen')
| -rw-r--r-- | api_docgen/Makefile.docfiles | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/api_docgen/Makefile.docfiles b/api_docgen/Makefile.docfiles index d6dc10df29..e403da657a 100644 --- a/api_docgen/Makefile.docfiles +++ b/api_docgen/Makefile.docfiles @@ -34,11 +34,8 @@ thread_MLIS := \ thread.mli event.mli \ threadUnix.mli -STDLIB=$(filter-out stdlib__pervasives, $(STDLIB_MODULES)) - -stdlib_UNPREFIXED=$(STDLIB:stdlib__%=%) libref= \ - $(stdlib_UNPREFIXED) \ + $(filter-out pervasives,$(STDLIB_MODULE_BASENAMES)) \ $(str_MLIS:%.mli=%) \ $(unix_MLIS:%.mli=%) \ $(dynlink_MLIS:%.mli=%) \ |