diff options
| author |  Guido Vranken <guidovranken@users.noreply.github.com> | 2022-07-08 04:27:27 +0200 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2022-07-08 12:27:27 +1000 |
| commit | ae357f3b77288a8bd6ffd1e18e9d2e9009d0afaf (patch) | |
| tree | 2882081f2508d8f1da411058380b8f3b09d172bf /projects | |
| parent | 402f3a1fb1690c06aea966e2576c4233da5dc738 (diff) | |
[bls-signatures] Fix build (#7976)
Diffstat (limited to 'projects')
| -rwxr-xr-x | projects/bls-signatures/build.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/projects/bls-signatures/build.sh b/projects/bls-signatures/build.sh index 6c9beca0..27eb1e93 100755 --- a/projects/bls-signatures/build.sh +++ b/projects/bls-signatures/build.sh @@ -164,6 +164,7 @@ fi if [[ "$SANITIZER" != "memory" ]] then cd $SRC/mcl/ + make bint_header mkdir build/ cd build/ if [[ $CFLAGS != *-m32* ]] |