jenkins_arch.sh: Accept "arm-none-eabi" as alias for "arm"
The jenkins build job is calling the script using "amd64" and
"arm-none-eabi", while the script expects "amd64" and "arm".
Let's add "arm-none-eabi" as an alias for "arm".
Closes: OS#3360
Change-Id: Idedd4778a63d67cdbf4f4d538bf4a225abb7547a
diff --git a/contrib/jenkins_arch.sh b/contrib/jenkins_arch.sh
index 360fd1c..cf9546e 100755
--- a/contrib/jenkins_arch.sh
+++ b/contrib/jenkins_arch.sh
@@ -22,7 +22,7 @@
./contrib/jenkins_amd64.sh
;;
- arm)
+ arm|arm-none-eabi)
./contrib/jenkins_arm.sh
;;