Follow up of #7266 (comment) Replace the convoluted Makefile in contrib/devtools/ with a separate (almost) idempotent install script.
Follow up of #7266 (comment) Replace the convoluted Makefile in contrib/devtools/ with a separate (almost) idempotent install script.