# ar: Bad file number
# see #3201. We need to specify a smaller max command-line size
# to work around it. 32767 doesn't work; 30000 does.
# ar: Bad file number
# see #3201. We need to specify a smaller max command-line size
# to work around it. 32767 doesn't work; 30000 does.