From a6095e7d3990dc518d3f7f14dbae6dc9ed8ddb8d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 7 Dec 2023 12:09:00 +0200 Subject: [PATCH] Use (include_subdirs no) for new dune libraries --- src/config/dune | 2 +- src/domain/dune | 2 +- src/incremental/dune | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/config/dune b/src/config/dune index b4dfea5c18..1508e2553e 100644 --- a/src/config/dune +++ b/src/config/dune @@ -1,4 +1,4 @@ -(include_subdirs unqualified) +(include_subdirs no) (library (name goblint_config) diff --git a/src/domain/dune b/src/domain/dune index 45345b5946..169f4a1d5c 100644 --- a/src/domain/dune +++ b/src/domain/dune @@ -1,4 +1,4 @@ -(include_subdirs unqualified) +(include_subdirs no) (library (name goblint_domain) diff --git a/src/incremental/dune b/src/incremental/dune index a664c78ea7..595dba22f7 100644 --- a/src/incremental/dune +++ b/src/incremental/dune @@ -1,4 +1,4 @@ -(include_subdirs unqualified) +(include_subdirs no) (library (name goblint_incremental)