[ARI patch] Fix gawk-4.0 warning

[Joel Brobecker]

> Didn't we talk at some point about moving the script over to the GDB
> repo?  It'd be nice to have it a bit more integrated with GDB so
> people more easily run it locally..

I think this one can be moved, yeah.  The others might be less useful
because they are just glue between the way things are stored on
sourceware, and the configure/Makefile code in GDB.

-- 
Joel