From a0b11f48e6e879eb811cb9f29e1bb817da1b3525 Mon Sep 17 00:00:00 2001
From: Gabriel Kerneis
Date: Thu, 26 Jun 2014 16:53:12 +0100
Subject: Remove .native in make clean

---
 src/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Makefile b/src/Makefile
index a8aeb1a4..8d3c1b9c 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -23,7 +23,7 @@ test_idempotence: sail
 
 clean:
 	-ocamlbuild -clean
-	-rm -rf _build
+	-rm -rf _build *.native
 	-rm -rf html-doc
 	-rm -rf tex-doc
 	-rm -rf lem lib
-- 
cgit v1.2.3