aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-13 17:03:49 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-11-13 17:03:49 -0500
commita02b6fc736299eb90e03640a9d2902a128ad07ae (patch)
tree9e438c884dd8e16d7403efb7bbe63acb878a0180 /src
parent6b644cdc4cb71b36f5cf354b12f1345fc4dd392e (diff)
Don't copy bounds files if no argument is passed
Diffstat (limited to 'src')
-rwxr-xr-xsrc/SpecificGen/copy_bounds.sh5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/SpecificGen/copy_bounds.sh b/src/SpecificGen/copy_bounds.sh
index 5c883ad18..ec7821d19 100755
--- a/src/SpecificGen/copy_bounds.sh
+++ b/src/SpecificGen/copy_bounds.sh
@@ -7,6 +7,11 @@ cd "$DIR"
FILENAME="$1"
V_FILE_STEM="${FILENAME%.*}"
+if [ -z "$V_FILE_STEM" ]; then
+ echo "USAGE: $0 JSON_FILE"
+ exit 1
+fi
+
for ORIG in $(git ls-files "../Specific/**GF25519*.v" | grep -v "../Specific/GF25519.v"); do
NEW="$(echo "$ORIG" | sed s'|^../Specific|.|g' | sed s"|25519|${V_FILE_STEM}|g")"
echo "$NEW"