From 7e59d2723fb9c5b4631f5eac1e99ae8956871a7f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 29 Jun 2020 16:59:31 +0100 Subject: Develop compiles again --- Makefile | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 3d31b2f..1303b13 100644 --- a/Makefile +++ b/Makefile @@ -67,3 +67,4 @@ clean:: Makefile.coq clean:: rm -f */*.v.d */*.glob */*.vo */*~ *~ + rm -f src/extraction/*.ml src/extraction/*.mli -- cgit