Skip to content

Instantly share code, notes, and snippets.

@nobrowser

nobrowser/dune.bash

Last active November 27, 2022 18:14
Show Gist options
  • Save nobrowser/895ef23b0805a7003ecf68e965368884 to your computer and use it in GitHub Desktop.
Save nobrowser/895ef23b0805a7003ecf68e965368884 to your computer and use it in GitHub Desktop.
Download ZIP
Wrapper around dune to direct output to stdin and remove frills
Raw
dune.bash
#/usr/local/bin/bash -Cfu
# bash only because of PIPESTATUS
eval `opam env --shell=bash` || exit 1
unset INSIDE_EMACS
dune "$@" 2>&1 | cat
exit ${PIPESTATUS[0]}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment