From f51ca395d8655f2dd3a1137c25e448a5a91a6c3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Fri, 14 Oct 2011 13:39:10 +0200
Subject: [PATCH] script to clean the compiler binaries

To refresh everything, it is now sufficient
first clean_heptc
second use heptc
---
 clean_heptc | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100755 clean_heptc

diff --git a/clean_heptc b/clean_heptc
new file mode 100755
index 0000000..3f3227b
--- /dev/null
+++ b/clean_heptc
@@ -0,0 +1,2 @@
+#!/bin/sh
+rm -rf compiler/heptc.byte compiler/heptc.d.byte compiler/_build