File: exec.sh

package info (click to toggle)
menhir 20210929-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, sid
  • size: 4,292 kB
  • sloc: ml: 24,825; sh: 180; makefile: 100; lisp: 8
file content (35 lines) | stat: -rwxr-xr-x 919 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
#!/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