From ed996432fd079583afbb1797c92ad23f654b94eb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 8 Mar 2019 16:30:30 +0100
Subject: [dune] typo

---
 dev/doc/build-system.dune.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index b1bfac8cc9..49251d61a1 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -22,7 +22,7 @@ If you want to build the standard libraries and plugins you should
 call `make -f Makefile.dune voboot`. It is usually enough to do that
 once per-session.
 
-More helper targets are availabe in `Makefile.dune`, `make -f
+More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
 Dune places build artifacts in a separate directory `_build`; it will
-- 
cgit v1.2.3


From 55e89d725cad4714d61c1201478c4b2ae786d070 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 13 Mar 2019 11:09:41 +0100
Subject: overlay for ltac2

---
 dev/ci/user-overlays/09733-gares-quotations.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/09733-gares-quotations.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh
new file mode 100644
index 0000000000..b17454fc4c
--- /dev/null
+++ b/dev/ci/user-overlays/09733-gares-quotations.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then
+
+    ltac2_CI_REF=quotations
+    ltac2_CI_GITURL=https://github.com/gares/ltac2
+
+fi
-- 
cgit v1.2.3