tests/playground/run.sh - third_party/github.com/leanprover/lean4 - Git at Google


            
            #!/usr/bin/env bash

            
            if [ $# -eq 0 ]; then

            
                echo "Usage: run.sh [file] [args]*"

            
                exit 1

            
            fi

            
            ff=$1

            
            ./compile.sh $ff

            
            shift 1

            
            time "./$ff.out" $*
	#!/usr/bin/env bash
	if [ $# -eq 0 ]; then
	echo "Usage: run.sh [file] [args]*"
	exit 1
	fi
	ff=$1
	./compile.sh $ff
	shift 1
	time "./$ff.out" $*