nightly: build headers before installing them
commitd2864e852be06ea7cb3478de3650ec36308ad934
authorJosef 'Jeff' Sipek <jeffpc@josefsipek.net>
Mon, 3 Sep 2018 22:31:01 +0000 (3 18:31 -0400)
committerJosef 'Jeff' Sipek <jeffpc@josefsipek.net>
Mon, 3 Sep 2018 22:38:27 +0000 (3 18:38 -0400)
tree213f70423908d9b2e4d5a3188c82f011875a466e
parentc3586fe88aaeda6c237ac9a2d51a77a91c9ddeee
nightly: build headers before installing them

Otherwise, we risk nightly failing because the xdrgen'd headers not yet
existing.
tools/nightly.sh