sidekick.sh: make dune phase silent

This commit is contained in:
Simon Cruanes 2022-07-18 23:28:45 -04:00
parent 6dca63b0ea
commit 729c72a27d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4

View file

@ -1,3 +1,3 @@
#!/bin/sh #!/bin/sh
OPTS=--profile=release OPTS="--profile=release --display=quiet"
exec dune exec $OPTS ./src/main/main.exe -- $@ exec dune exec $OPTS ./src/main/main.exe -- $@