solved doc issue because generate_doc was nondet

543ec9c2 · SOLIMAN Sylvain · 341894d3 · 543ec9c2
Commit 543ec9c2 authored Dec 02, 2019 by SOLIMAN Sylvain
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 2 deletions

doc.pl doc.pl +4 -2

No files found.
--- a/doc.pl
+++ b/doc.pl
@@ -908,13 +908,15 @@ setup_doc :-
 generate_doc :-
  setup_doc,
  generate_doc_file(doc),
-  check_doc(doc, quiet).
+  check_doc(doc, quiet),
+  !.


 generate_devdoc :-
  setup_doc,
  generate_doc_file(devdoc),
-  check_doc(devdoc, quiet).
+  check_doc(devdoc, quiet),
+  !.


 generate_doc_file(Type) :-