From 5034e31325934160813d06437afc16717f5d9a8b Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 13 Dec 2021 16:23:10 +0100
Subject: [PATCH] remove test section of makefile
---
proofs/pipeline/Makefile | 6 ------
1 file changed, 6 deletions(-)
diff --git a/proofs/pipeline/Makefile b/proofs/pipeline/Makefile
index c6d8571..0f9eb4e 100644
--- a/proofs/pipeline/Makefile
+++ b/proofs/pipeline/Makefile
@@ -1,11 +1,5 @@
ROOT = pipe
CMDLINER = true
-.PHONY: _tests
-_tests:
- (cd examples && ${MAKE})
-
-tests: _tests
-
.include "../dune-exe.mk"
.include "../tools.mk"
--
GitLab