Fix pgarm64 hostname
authorChristoph Berg <myon@debian.org>
Thu, 18 Jul 2024 12:40:30 +0000 (14:40 +0200)
committerChristoph Berg <myon@debian.org>
Thu, 18 Jul 2024 12:40:30 +0000 (14:40 +0200)
jenkins/ansible/hosts

index f868d0d249b670e8bd20b8d7757848eda7bad2b3..fb2c5d08f05ca82016ceee61aa149e954338c0d4 100644 (file)
@@ -1,6 +1,6 @@
 pgdgbuild.dus.dg-i.net chroot_dir=/home/chroot.buexcl run_opts="size=20G"
 pgx86 chroot_dir=/home/chroot run_opts="size=50G"
-pgdgbuild-arm64 chroot_dir=/home/chroot run_opts="size=50G"
+pgarm64 chroot_dir=/home/chroot run_opts="size=50G"
 # ppc64el: 24GB is not enough to build postgis with 4 workers (huge B-Ds)
 pgppc64el chroot_dir=/home/chroot run_opts="size=100G,nr_inodes=800k"
 pgs390x chroot_dir=/home/chroot run_opts="size=100G,nr_inodes=800k"