diff --git a/http_of_dir.sh b/http_of_dir.sh index f9ba2a7b..a2338d18 100755 --- a/http_of_dir.sh +++ b/http_of_dir.sh @@ -1,2 +1,3 @@ #!/bin/sh -exec dune exec ./src/bin/http_of_dir.exe -- $@ +OPTS="--display=quiet --profile=release" +exec dune exec $OPTS ./src/bin/http_of_dir.exe -- $@