Exclude doc from default dune alias

goblint · Jul 16, 2022 · 3d79fd3 · 3d79fd3
1 parent 662247a
commit 3d79fd3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/dune b/dune
@@ -0,0 +1,3 @@
+(alias
+ (name default)
+ (deps (alias_rec bin/all) (alias_rec lib/all) (alias_rec src/all) (alias_rec test/all))) ; everything but doc