From 57f62f06419972ba799e451d2f56552dc1b2fb63 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 15:42:18 +0100
Subject: [plugin] Remove LocalityFixme über hack.

To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.

This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
---
 dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
new file mode 100644
index 0000000000..c9f1272bed
--- /dev/null
+++ b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then
+    ltac2_CI_BRANCH=localityfixyou
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git
+fi
-- 
cgit v1.2.3