From 54d43d34f7867b55a6135f7b28b44e1d74d2d839 Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Mon, 19 Jun 2023 09:42:14 +0200 Subject: [PATCH] doc: commit promoted doc/dune.inc This is a leftover from #7985. Signed-off-by: Etienne Millon --- doc/dune.inc | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/doc/dune.inc b/doc/dune.inc index 62dc3bd1d2c..9392d353b36 100644 --- a/doc/dune.inc +++ b/doc/dune.inc @@ -1,4 +1,13 @@ +(rule + (with-stdout-to dune-printenv.1 + (run dune printenv --help=groff))) + +(install + (section man) + (package dune) + (files dune-printenv.1)) + (rule (with-stdout-to dune-promote.1 (run dune promote --help=groff))) @@ -179,15 +188,6 @@ (package dune) (files dune-pkg.1)) -(rule - (with-stdout-to dune-printenv.1 - (run dune printenv --help=groff))) - -(install - (section man) - (package dune) - (files dune-printenv.1)) - (rule (with-stdout-to dune-promotion.1 (run dune promotion --help=groff))) @@ -224,6 +224,15 @@ (package dune) (files dune-runtest.1)) +(rule + (with-stdout-to dune-show.1 + (run dune show --help=groff))) + +(install + (section man) + (package dune) + (files dune-show.1)) + (rule (with-stdout-to dune-shutdown.1 (run dune shutdown --help=groff)))