diff options
Diffstat (limited to 'jenkins-helpers.sh')
-rw-r--r-- | jenkins-helpers.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 71d60a22..473d16e2 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -1017,6 +1017,7 @@ print_gnu_target () fi case "$target" in "aarch64") target="aarch64-linux-gnu" ;; + "arm-eabi") target="arm-eabi" ;; "arm"*) target="arm-linux-gnueabihf" ;; "x86_64") target="x86_64-linux-gnu" ;; *) echo "ERROR: Unknown target $target" >&2; exit 1 ;; |