From 162e63030c97fa5cbb8e5706dd348f0b2f2c6902 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 13 Jul 2020 21:37:42 +0200
Subject: [PATCH] leanmake: allow setting linker options

---
 src/lean.mk.in | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/lean.mk.in b/src/lean.mk.in
index b4bb49dc2c..e8052f2cee 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -19,6 +19,7 @@ BIN_NAME = $(PKG)
 STATIC_LIB_NAME = lib$(PKG).a
 LEAN_OPTS = @LEAN_EXTRA_MAKE_OPTS@
 LEANC_OPTS = -O3 -DNDEBUG
+LINK_OPTS =
 
 SRCS = $(shell find $(PKG) -name '*.lean' 2> /dev/null || true; find $(PKG).lean 2> /dev/null)
 DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend))
@@ -73,7 +74,7 @@ $(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Linking $@"
 endif
-	leanc -o "$@" -x none $^
+	leanc -o "$@" -x none $^ $(LINK_OPTS)
 
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
 	@rm -f $@