diff options
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index dd27cfcbdd..6ed452dce8 100644 --- a/Makefile.build +++ b/Makefile.build @@ -910,7 +910,7 @@ endif $(HIDE)$(OCAMLYACC) $< %_mod.ml: %.mllib - sed -e "s/\([^ ]\+\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ + sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ %.ml4-preprocessed: %.ml4 | %.ml4.d |