From f6dbdf7ac372eccd3f1fe5e00d37402399e2e256 Mon Sep 17 00:00:00 2001 From: Pietro Date: Tue, 20 Mar 2018 17:53:33 +0100 Subject: [PATCH] Test: fix make fix-indent erase all problem --- src/lib_stdlib/test-ocp-indent.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/lib_stdlib/test-ocp-indent.sh b/src/lib_stdlib/test-ocp-indent.sh index a5d7b8c13..d1e44de5a 100755 --- a/src/lib_stdlib/test-ocp-indent.sh +++ b/src/lib_stdlib/test-ocp-indent.sh @@ -1,5 +1,11 @@ #!/bin/bash +type ocp-indent > /dev/null 2>&- +if [ $? -ne 0 ]; then + echo "I require ocp-indent but it's not installed (opam install ocp-indent). Aborting." + exit 1 +fi + tmp_dir="$(mktemp -d -t tezos_build.XXXXXXXXXX)" failed=no if [ "$1" = "fix" ]; then