From 72926462e4f24d558c6ecc7c0ad773427905b3d1 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 13 Dec 2017 02:46:59 -0500
Subject: Add missing file from previous commit

---
 etc/ci/remove_autogenerated.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100755 etc/ci/remove_autogenerated.sh

(limited to 'etc')

diff --git a/etc/ci/remove_autogenerated.sh b/etc/ci/remove_autogenerated.sh
new file mode 100755
index 000000000..26f4f087e
--- /dev/null
+++ b/etc/ci/remove_autogenerated.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+cd "$( dirname "${BASH_SOURCE[0]}" )"
+cd ../..
+sed s'|^src/Specific/montgomery.*||g' -i _CoqProject
+sed s'|^src/Specific/solinas.*||g' -i _CoqProject
-- 
cgit v1.2.3