Use bash instead of sh for pages build

This commit is contained in:
Sumner Evans
2020-01-20 22:06:28 -07:00
parent 2eda579830
commit b458781c03
2 changed files with 6 additions and 3 deletions

View File

@@ -1,4 +1,6 @@
#! /bin/sh
#! /usr/bin/env bash
set -xe
pushd docs
pipenv run make html