From 5584491034aba5b3e75454f77a61968eccd9a119 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 18 Nov 2022 10:18:11 +0000
Subject: [PATCH] Apply remarks from @maroneze
---
doc/developer/advance.tex | 10 +++++-----
doc/developer/tutorial/hello/src/Makefile | 2 +-
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 49e246def29..6cae8c5de9a 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -192,7 +192,7 @@ Note that \verb|camlp5| is not among the dependencies declared in
Since the adoption of Dune, \framac's \texttt{Makefile}s were largely
simplified. They are still used for some tasks, partially due to conciseness
(\verb|make| is shorter than \verb|dune build|), partially because some tasks
-are better suited for them. Some standards targets are defined in various
+are better suited for them. Some standard targets are defined in various
Makefiles that are installed in \framac's shared directory.
A minimal plugin's \verb|Makefile| can thus be the following:
@@ -825,9 +825,9 @@ one for regular tests (if more than one \verb|OPT|).\\
\hline
\verb|PTEST_ORACLE| & basename of the current oracle file (macro only usable in FILTER directives)\\
\hline
-\verb|PTEST_MODULE| & current list of module defined by the \verb|MODULE| directive\\
+\verb|PTEST_MODULE| & current list of modules defined by the \verb|MODULE| directive\\
\hline
-\verb|PTEST_LIBS| & current list of module defined by the \verb|LIBS| directive\\
+\verb|PTEST_LIBS| & current list of modules defined by the \verb|LIBS| directive\\
\hline
\verb|PTEST_PLUGIN| & current list of plugins defined by the \verb|PLUGIN| directive\\
\hline
@@ -4196,9 +4196,9 @@ the \texttt{opam} integration within
\texttt{dune}\footnote{\url{https://dune.readthedocs.io/en/stable/opam.html}}.
Basically, the \index{dune-project}\texttt{dune-project} file
(see Section~\ref{tut2:hello}) should contain a stanza
-\texttt{(generate\_opam\_files true)}, as well as a few meta-information
+\texttt{(generate\_opam\_files true)}, as well as some meta-information
(location of the sources, licence, author(s), etc.). It is also possible to
-provide these information into a file \texttt{my-plugin-package.opam.template},
+provide this information in a file \texttt{my-plugin-package.opam.template},
assuming \texttt{my-plugin-package} is the name of the package of the plug-in in
the \texttt{dune-project} file. See the dune documentation for detailed information
about the creation of the \texttt{opam} file.
diff --git a/doc/developer/tutorial/hello/src/Makefile b/doc/developer/tutorial/hello/src/Makefile
index 61d832e1315..5c30410ff80 100644
--- a/doc/developer/tutorial/hello/src/Makefile
+++ b/doc/developer/tutorial/hello/src/Makefile
@@ -1,4 +1,4 @@
-FRAMAC_SHARE:=$(shell frama-c -print-share-path)
+FRAMAC_SHARE:=$(shell frama-c-config -print-share-path)
sinclude ${FRAMAC_SHARE}/Makefile.common
--
GitLab