aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
AgeCommit message (Collapse)Author
2017-12-26Delete old overlays (leaving example)Gaëtan Gilbert
2017-11-22[plugin] Remove LocalityFixme über hack.Emilio Jesus Gallego Arias
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.