js: measuring make check
time is not useful, especially not in a web browser
This commit is contained in:
parent
5eed910c11
commit
7afd929e70
@ -117,7 +117,7 @@ else
|
|||||||
mv -f "${file}.tmp" "$file"
|
mv -f "${file}.tmp" "$file"
|
||||||
done
|
done
|
||||||
)
|
)
|
||||||
time make $MAKE_FLAGS check || exit 1
|
make $MAKE_FLAGS check || exit 1
|
||||||
touch "$DONE_FILE"
|
touch "$DONE_FILE"
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user