From 6f4967549fd46cf4fcdcd5ff47fa2d14cf807a7a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <guillaume.melquiond@inria.fr> Date: Sun, 24 Jun 2018 09:28:47 +0200 Subject: [PATCH] Avoid warning messages when generating the gallery. --- Makefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.in b/Makefile.in index 55dc7b4f0..db47d8b9b 100644 --- a/Makefile.in +++ b/Makefile.in @@ -708,7 +708,7 @@ gallery-subs:: echo "exporting examples/$$d"; \ mkdir -p $(GALLERYDIR)/$$d; \ cd examples/$$d; \ - WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ *.mlw -o $(GALLERYDIR)/$$d; \ + WHY3CONFIG="" ../../bin/why3doc.@OCAMLBEST@ -L ../../stdlib -L . --stdlib-url http://why3.lri.fr/stdlib/ --debug ignore_unused_vars *.mlw -o $(GALLERYDIR)/$$d; \ cd ..; \ rm -f $(GALLERYDIR)/$$d/$$d.zip; \ git archive --format=zip -o $(GALLERYDIR)/$$d/$$d.zip HEAD $$d; \ -- GitLab