From d3d75740647c5bc83526b2a33efcc16052d87834 Mon Sep 17 00:00:00 2001 From: swrup Date: Wed, 11 Mar 2026 14:17:52 +0100 Subject: [PATCH] --- GNUmakefile | 6 ++++++ source.sh | 1 + 2 files changed, 7 insertions(+) create mode 100644 GNUmakefile create mode 100644 source.sh diff --git a/GNUmakefile b/GNUmakefile new file mode 100644 index 00000000..71dc157c --- /dev/null +++ b/GNUmakefile @@ -0,0 +1,6 @@ +vendor_list := mkernel miou zarith + +vendors: + @for v in $(vendor_list); do \ + [ ! -d "vendors/$v" ] && opam source $v --dir vendors/$v + done diff --git a/source.sh b/source.sh new file mode 100644 index 00000000..a9bf588e --- /dev/null +++ b/source.sh @@ -0,0 +1 @@ +#!/bin/bash