force disable gui on macOS

7cbff69e · Andre Maroneze · 8bec5d80 · 7cbff69e
Commit 7cbff69e authored 1 year ago by Andre Maroneze
--- a/opam
+++ b/opam
@@ -92,6 +92,7 @@ tags: [

 build: [
  ["bash" "dev/disable-plugins.sh" "e-acsl"] { os-family = "windows" }
+  ["bash" "dev/disable-plugins.sh" "gui"] { os = "macos" }
  ["dune" "build" "-j%{jobs}%" "--release" "--promote-install-files=false"
   "@install"
   "@doc" { with-doc }