Continue changes suggested by Julien’s review

doc/developer/changes.tex

@@ -8,8 +8,8 @@ This chapter summarizes the major changes in this documentation between each
 \section*{\framacversion}
 
 \begin{itemize}
-\item \textbf{Tutorial}: Update and completion of the Hello plug-in section
-along with the ability to generate the plug-in by \texttt{make archives}.
+\item \textbf{Tutorial}: Update and complete the Hello plug-in section
+along with making it available online.
 \item \textbf{Testing}: Explain the appropriate way to handle compilation
 of \texttt{.ml} scripts during tests
 \item \textbf{Makefiles}: Remove any reference to obsolete

doc/developer/developer.tex

@@ -44,8 +44,8 @@
 \vfill
 \title{Plug-in Development Guide}%
 {Release \framacversion}
-\author{Julien~Signoles with Loïc Correnson, Matthieu Lemerre and Virgile 
-Prevosto}
+\author{Julien~Signoles with Thibaud~Antignac, Loïc~Correnson, Matthieu~Lemerre
+and Virgile~Prevosto}
 \begin{center}
 CEA LIST, Software Security Laboratory, Saclay,F-91191
 \end{center}

doc/developer/tutorial.tex

@@ -508,9 +508,9 @@ presents how to properly test plug-ins.
 \subsection{Testing your Plug-in}\label{tut2:testing}
 \index{Plug-in!Testing}\index{Test}
 
-Frama-C supports non-regression testing of plug-ins. This is useful for
-non-regression and test-driven development purposes. The tool allowing to
-perform the tests is called \ptests\index{Ptests}.
+Frama-C supports non-regression testing of plug-ins. This is useful to check
+that further plug-in modifications do not introduce new bugs. The tool allowing
+to perform the tests is called \ptests\index{Ptests}.
 
 To build these tests, the location of the subdirectories containing them must
 be indicated in the \texttt{Makefile} through the variable
@@ -586,7 +586,7 @@ Then, \texttt{Command} shows the executed command for this test case followed
 by bash pipes to control the dataflow. (Note the \texttt{-hello}
 option which has been passed to \framac as requested by \texttt{OPT: -hello}
 in the \texttt{run.config}.)
-Two outputs are considered for each tests:
+Two outputs are considered as results for each test:
 an \emph{error} output and a \emph{result} output.
 These outputs are logged in the two following files:
 \texttt{./tests/hello/result/hello\_test.err.log} and

doc/developer/tutorial/hello/src/run_with_options.ml

@@ -6,7 +6,7 @@ let run () =
         Self.result "%s" msg
       else
         let chan = open_out filename in
-        Printf.fprintf chan "%s\n" msg;
+        Format.fprintf chan "%s@." msg;
         close_out chan
     in
     output_fun "Hello, world!"