From 2a74da7b6f275634fd8ed9c209edc73f2ae15427 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 16:38:52 +0200
Subject: Adding a file for testing typing.

---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index cfdeeba747..d555fea236 100644
--- a/Makefile
+++ b/Makefile
@@ -10,3 +10,7 @@ clean: Makefile.coq
 
 Makefile.coq: _CoqProject
 	$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
-- 
cgit v1.2.3