From 0fef89d4ef36cc6878626f0af5c9fa0780f2c735 Mon Sep 17 00:00:00 2001 From: "Glenn Y. Rolland" Date: Tue, 26 Jul 2016 23:25:03 +0200 Subject: [PATCH] Add makefile. --- .gitignore | 1 + Makefile | 16 ++++++++++++++++ the-bridge/Makefile | 1 + 3 files changed, 18 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 120000 the-bridge/Makefile diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e35d885 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +_build diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..4431722 --- /dev/null +++ b/Makefile @@ -0,0 +1,16 @@ + + +ML_FILES=$(wildcard *.ml) +NATIVE_FILES=$(patsubst %.ml,%.native,$(ML_FILES)) + +all: build + +build: $(NATIVE_FILES) + +clean: + rm -f $(NATIVE_FILES) + +%.native: %.ml + corebuild $@ + +.PHONY: all build clean diff --git a/the-bridge/Makefile b/the-bridge/Makefile new file mode 120000 index 0000000..d0b0e8e --- /dev/null +++ b/the-bridge/Makefile @@ -0,0 +1 @@ +../Makefile \ No newline at end of file