From 6573530dae30b1dd9e384fe48ec3e0e43f248fec Mon Sep 17 00:00:00 2001 From: Hugo Heuzard Date: Fri, 21 Jul 2023 17:19:00 +0200 Subject: [PATCH] fix --- .github/workflows/build.yml | 3 +++ dune-workspace | 6 ------ 2 files changed, 3 insertions(+), 6 deletions(-) delete mode 100644 dune-workspace diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 07d5545e2e..30136f56fb 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,5 +1,8 @@ name: build +env: + DUNE_CONFIG__BACKGROUND_DIGESTS: disabled + on: pull_request: push: diff --git a/dune-workspace b/dune-workspace deleted file mode 100644 index aa57780bad..0000000000 --- a/dune-workspace +++ /dev/null @@ -1,6 +0,0 @@ -(lang dune 3.7) - -(env - (_ - (env-vars - (DUNE_CONFIG__BACKGROUND_DIGESTS disabled))))