aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
diff options
context:
space:
mode:
authorThéo Zimmermann2019-08-24 08:36:25 +0200
committerThéo Zimmermann2019-08-24 08:36:25 +0200
commit07c4c8cac353883a2c6ae493556b9b544f3f38c0 (patch)
treef763366888c754728dada610d482e417cffdfb6f /doc/sphinx/practical-tools
parentadcbcbe743e0508a1fc3cd3eb18f73b00db1d55e (diff)
parenta5b7ca5eadc5cf1c2e431ea8b540006ff063e5b8 (diff)
Merge PR #10698: [dune] Migrate static Dune files to Dune 1.10
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/sphinx/practical-tools')
-rw-r--r--doc/sphinx/practical-tools/utilities.rst5
1 files changed, 1 insertions, 4 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 554f6bf230..47ecfb9db0 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -522,10 +522,7 @@ of your project.
(flags :standard -warn-error -3-9-27-32-33-50)
(libraries coq.plugins.cc coq.plugins.extraction))
- (rule
- (targets g_equations.ml)
- (deps (:pp-file g_equations.mlg))
- (action (run coqpp %{pp-file})))
+ (coq.pp (modules g_equations))
And a Coq-specific part that depends on it via the ``libraries`` field: