diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-25 13:06:30 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-25 13:06:30 -0500 |
| commit | 35436de8e023576c38f9b4c9d4539d90b679c2ce (patch) | |
| tree | f9b2ebe5efe5758e1f0ab549c95bac47105e05f2 /src/SpecificGen/copy_bounds.sh | |
| parent | fbdd082f2b7fab1fb5b074e193f1072d2ecdb2f7 (diff) | |
Also git add in copy_bounds
Diffstat (limited to 'src/SpecificGen/copy_bounds.sh')
| -rwxr-xr-x | src/SpecificGen/copy_bounds.sh | 4 |
1 files changed, 4 insertions, 0 deletions
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 |