diff options
Diffstat (limited to 'scripts/doc-build.sh')
-rwxr-xr-x | scripts/doc-build.sh | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/scripts/doc-build.sh b/scripts/doc-build.sh index 98dfa82f6..18f4e6ca8 100755 --- a/scripts/doc-build.sh +++ b/scripts/doc-build.sh @@ -32,6 +32,32 @@ if ! [ -x node_modules/.bin/ronn ]; then fi fi +if ! [ -x node_modules/.bin/marked ]; then + ps=0 + if [ -f .building_marked ]; then + pid=$(cat .building_marked) + ps=$(ps -p $pid | grep $pid | wc -l) || true + fi + + if [ -f .building_marked ] && [ $ps != 0 ]; then + while [ -f .building_marked ]; do + sleep 1 + done + else + # a race to see which make process will be the one to install marked + echo $$ > .building_marked + sleep 1 + if [ $(cat .building_marked) == $$ ]; then + make node_modules/.bin/marked + rm .building_marked + else + while [ -f .building_marked ]; do + sleep 1 + done + fi + fi +fi + src=$1 dest=$2 name=$(basename ${src%.*}) |