From 7e014333c57bdede663e490743bc84f696764381 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 14 Sep 2018 14:27:39 +0000
Subject: Helpers for debugging external projects from CI

---
 dev/ci/nix/shell | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100755 dev/ci/nix/shell

(limited to 'dev/ci/nix/shell')

diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
new file mode 100755
index 0000000000..2e4462ed40
--- /dev/null
+++ b/dev/ci/nix/shell
@@ -0,0 +1,20 @@
+#!/usr/bin/env sh
+
+## This file should be run from the root of the Coq source tree
+
+BRANCH=$(git rev-parse --abbrev-ref HEAD)
+echo "Branch: $BRANCH in $PWD"
+
+if [ "$#" -ne 1 ]; then
+  PROJECT=""
+else
+  PROJECT="--argstr project $1"
+fi
+
+if [ "$BN" ]; then
+  BN="--argstr bn ${BN}"
+else
+  BN=""
+fi
+
+nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN
-- 
cgit v1.2.3