10 lines
87 B
Bash
10 lines
87 B
Bash
#!/bin/bash
|
|
|
|
set -xe
|
|
|
|
THIS=$(dirname "$0")
|
|
|
|
pushd ${THIS}/../
|
|
make -C doc/ dist
|
|
popd
|