20 lines
757 B
Bash
Executable file
20 lines
757 B
Bash
Executable file
#!/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`
|
|
|
|
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[@]}" "$@"
|