From 35436de8e023576c38f9b4c9d4539d90b679c2ce Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 25 Nov 2016 13:06:30 -0500
Subject: Also git add in copy_bounds

---
 src/SpecificGen/copy_bounds.sh | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/SpecificGen/copy_bounds.sh')

diff --git a/src/SpecificGen/copy_bounds.sh b/src/SpecificGen/copy_bounds.sh
index 0c73ac268..bb43e1aaa 100755
--- a/src/SpecificGen/copy_bounds.sh
+++ b/src/SpecificGen/copy_bounds.sh
@@ -22,4 +22,8 @@ for ORIG in $(git ls-files "../Specific/**GF25519*.v" | grep -v "../Specific/GF2
     NEW_DIR="$(dirname "$NEW")"
     mkdir -p "$NEW_DIR" || exit $?
     cat "$ORIG" | sed s"/64/${BIT_WIDTH}/g" | sed s'/Specific/SpecificGen/g' | sed s"/25519/${V_FILE_STEM}/g" > "$NEW" || exit $?
+    if [ -z "$(git ls-files "$NEW")" ]; then
+        echo "git add '$NEW'"
+        git add "$NEW" || exit $?
+    fi
 done
-- 
cgit v1.2.3