pre_marking1/mk
changeset 382 1bd800376e0c
parent 376 6cc36d0ef79e
equal deleted inserted replaced
381:116fa3c8584f 382:1bd800376e0c
     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