diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index b92bf5c08af89d2787a2f28c09872cc0d19840cc..3aa40e5f9d34bb05d5296d13e370fb42bda538de 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -1023,7 +1023,7 @@ the sequence above is read in order and defines a configuration level STDOPT: [[+#-]"opt" ...] \end{code} options are always given between quotes. An option following a \texttt{+} -(resp. \texttt{\#} is added to the end (resp. start) of current set of options +(resp. \texttt{\#}) is added to the end (resp. start) of current set of options while an option following a \texttt{-} is removed from it. The directive can be empty (meaning that the corresponding test will use the standard set of options). As with \texttt{OPT}, each \texttt{STDOPT} corresponds to a different @@ -2938,9 +2938,9 @@ module Print = \end{ocamlcode} So it is a boolean parameter initialized by default to \texttt{false}. The declared interface for this module is simply -\scodeidx{Parameter\_sig}{Int} +\scodeidx{Parameter\_sig}{Bool} \begin{ocamlcode} -module Print: Parameter_sig.Int +module Print: Parameter_sig.Bool \end{ocamlcode} Another example is the parameter corresponding to the option diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex index 3a286b2e55755748867b94b4666871a76261ee27..a8551f1f9cba789e688fbcb579b579f7bec66fbf 100644 --- a/doc/developer/developer.tex +++ b/doc/developer/developer.tex @@ -101,8 +101,8 @@ described here may still evolve in the future. %\addcontentsline{toc}{chapter}{Acknowledgements} We gratefully thank all the people who contributed to this document: Gergö -Barany, Patrick -Baudin, Richard Bonichon, Pascal Cuoq, Zaynah Dargaye, Florent Garnier, +Barany, Patrick Baudin, Richard Bonichon, Pascal Cuoq, Zaynah Dargaye, Basile +Desloges, Florent Garnier, Pierre-Loïc Garoche, Philippe Herrmann, Boris Hollas, Nikolaï Kosmatov, Jean-Christophe Léchenet, André Maroneze, Benjamin Monate, Yannick Moy, Anne Pacalet, Armand Puccetti, Muriel Roger and Boris diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex index 76223c6ba9dee876603569a18ce7692ff5868d33..457004dd0a5643c0c65fbd40384b55d8085f3e9c 100644 --- a/doc/developer/tutorial.tex +++ b/doc/developer/tutorial.tex @@ -527,6 +527,7 @@ This enables the creation of a \texttt{./tests/ptests\_config} file holding the environement needed by \ptests to run the plug-in's tests by running: \begin{shell} +\$ mkdir tests \$ make <...> Generating tests/ptests_config