From 6a999080bb0eaeabb88e286020bcca39e8f21602 Mon Sep 17 00:00:00 2001 From: Etienne Millon Date: Thu, 3 Dec 2020 17:25:06 +0100 Subject: [PATCH] Build site and pdf by default Closes #3416 --- dune | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/dune b/dune index 6660269c0..0efd6a24a 100644 --- a/dune +++ b/dune @@ -1,2 +1,8 @@ (env (non-deterministic (env-vars (MDX_RUN_NON_DETERMINISTIC true)))) + +(alias + (name install) + (deps + (alias_rec site) + (alias_rec pdf)))