diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-13 17:03:49 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-13 17:03:49 -0500 |
commit | a02b6fc736299eb90e03640a9d2902a128ad07ae (patch) | |
tree | 9e438c884dd8e16d7403efb7bbe63acb878a0180 /src | |
parent | 6b644cdc4cb71b36f5cf354b12f1345fc4dd392e (diff) |
Don't copy bounds files if no argument is passed
Diffstat (limited to 'src')
-rwxr-xr-x | src/SpecificGen/copy_bounds.sh | 5 |
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" |