Commit 66e74da5 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

New script exec.sh to run just one test.

parent f94f3d37
Pipeline #188781 passed with stages
in 1 minute and 59 seconds
#!/bin/bash
set -euo pipefail
# This script re-runs a specific test, named on the command line.
# Examples:
# ./exec.sh good/mezzo
# ./exec.sh bad/option
# If this is a newly created test, then [make depend] should be run first
# for dune to know about this test.
for name in "$@"
do
if [[ $name =~ ^good/.* ]] ; then
# A positive test.
base=${name#good/}
rm -f _build/default/test/static/"$name".out
dune build @$base
# Display the timings.
cat _build/default/test/static/"$name".timings
elif [[ $name =~ ^bad/.* ]] ; then
# A negative test.
base=${name#bad/}
rm -f _build/default/test/static/"$name".out
dune build @$base
# Display the output.
cat _build/default/test/static/"$name".out
else
# Unrecognized.
echo "Don't know what to do with '$name'."
echo "This script handles tests whose name begins with good/ or bad/."
exit 1
fi
done
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment