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))))