Commit 2582e7bb06f1638877713400e2d11db547798a49

Bruno Haible 2022-07-18T19:33:52

Make autopull.sh more suited for continuous integration. * autopull.sh: Support option --one-time.