Allow the pull-docs script to pull other than master
authorBjørn Erik Pedersen <bjorn.erik.pedersen@gmail.com>
Sat, 23 Sep 2017 08:11:20 +0000 (10:11 +0200)
committerBjørn Erik Pedersen <bjorn.erik.pedersen@gmail.com>
Sat, 23 Sep 2017 08:13:40 +0000 (10:13 +0200)
commit9436f0b0c31d2df49647e301ab3d6e2053b356b8
treed78358e69389a8ab6c9dec5a15363668ecb47885
parentf8fd5796bb266352e61d897430c7659ce5d6565c
Allow the pull-docs script to pull other than master
pull-docs.sh