fix gnulib-tool botched merge