From 22ee430045eb2eace058b5b0ce2a16041839db0e Mon Sep 17 00:00:00 2001
From: Thibaud Antignac <thibaud.antignac@cea.fr>
Date: Thu, 26 Oct 2017 03:03:21 +0200
Subject: [PATCH] =?UTF-8?q?Continue=20changes=20suggested=20by=20Julien?=
 =?UTF-8?q?=E2=80=99s=20review?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 doc/developer/changes.tex                            | 4 ++--
 doc/developer/developer.tex                          | 4 ++--
 doc/developer/tutorial.tex                           | 8 ++++----
 doc/developer/tutorial/hello/src/run_with_options.ml | 2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index e8ed8ee4139..907ae9806ad 100644
--- a/doc/developer/changes.tex
+++ b/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
diff --git a/doc/developer/developer.tex b/doc/developer/developer.tex
index 9fe1c2603ea..2484fcdfb4e 100644
--- a/doc/developer/developer.tex
+++ b/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}
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index e182b1dd80a..8e0227a4f2b 100644
--- a/doc/developer/tutorial.tex
+++ b/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
diff --git a/doc/developer/tutorial/hello/src/run_with_options.ml b/doc/developer/tutorial/hello/src/run_with_options.ml
index fa07e2086a5..e3ab8d9b4ed 100644
--- a/doc/developer/tutorial/hello/src/run_with_options.ml
+++ b/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!"
-- 
GitLab