pre_marking1/mk
changeset 382 fec2c2f2d3db
parent 376 944db68cddbd
equal deleted inserted replaced
381:6c2792a3e00d 382:fec2c2f2d3db
     1 #!/bin/sh
     1 #!/bin/bash
     2 ###set -e
     2 set -euo pipefail
     3 
     3 
     4 trap "exit" INT
     4 trap "exit" INT
     5 
     5 
     6 files=${1:-*/pre1}
     6 files=${1:-*/pre1}
     7 
     7