From affd90247d952e2891b3195df1adc3b0b90a8561 Mon Sep 17 00:00:00 2001
From: Daniil Baturin <daniil@baturin.org>
Date: Tue, 13 Dec 2016 08:11:55 +0600
Subject: Remove oasis-generated files, not needed at least until we modify
 anything in them.

---
 configure | 27 ---------------------------
 1 file changed, 27 deletions(-)
 delete mode 100755 configure

(limited to 'configure')

diff --git a/configure b/configure
deleted file mode 100755
index 6acfaeb..0000000
--- a/configure
+++ /dev/null
@@ -1,27 +0,0 @@
-#!/bin/sh
-
-# OASIS_START
-# DO NOT EDIT (digest: dc86c2ad450f91ca10c931b6045d0499)
-set -e
-
-FST=true
-for i in "$@"; do
-  if $FST; then
-    set --
-    FST=false
-  fi
-
-  case $i in
-    --*=*)
-      ARG=${i%%=*}
-      VAL=${i##*=}
-      set -- "$@" "$ARG" "$VAL"
-      ;;
-    *)
-      set -- "$@" "$i"
-      ;;
-  esac
-done
-
-ocaml setup.ml -configure "$@"
-# OASIS_STOP
-- 
cgit v1.2.3