src/bin/leanmake

#!/usr/bin/env bash
# A simple wrapper around `make` and the `lean.mk` makefile
# When called from a directory containing a `Makefile` file, calls `make` with
# the directory containing `lean.mk` in its path so that you can use
# `include lean.mk` in your code. Otherwise, run `lean.mk` directly.
# Interesting targets:
# * `leanmake PKG=Foo`  # compile package Foo into .olean files (in `build/Foo`, by default)
# * `leanmake bin PKG=Foo`  # build the binary `build/bin/Foo`
# * `leanmake lib PKG=Foo`  # build the library `build/lib/libFoo.a`
# If there is exactly one .lean file in the current directory, you can omit `PKG`

set -euo pipefail

bindir=$(dirname $0)
if [ -f Makefile ]; then
    args=(-I "$bindir/../share/lean")
else
    args=(-f "$bindir/../share/lean/lean.mk")
fi

PATH="$bindir:$PATH" ${MAKE:-make} "${args[@]}" "$@"