From e3ac9e23b32d96a9063b02d8e6ac8f9c5e7cafae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 5 Dec 2024 11:01:52 +0100
Subject: [PATCH] opam: remove with-test commands

They are meant to be executed with an installed certicoq so won't work in the build step.
---
 coq-certicoq.opam | 2 --
 1 file changed, 2 deletions(-)

diff --git a/coq-certicoq.opam b/coq-certicoq.opam
index 90b5c0d2..3ba708d7 100644
--- a/coq-certicoq.opam
+++ b/coq-certicoq.opam
@@ -23,8 +23,6 @@ build: [
   [make "all"]
   [make "plugins"]
   [make "bootstrap"]
-  [make "-C" "benchmarks" "all"] {with-test}
-  [make "-C" "bootstrap" "tests"] {with-test}
 ]
 install: [
   [make "install"]