aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-24 23:05:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-25 01:16:09 +0200
commit94e783390ef9ad9d26a54add2287e0a3e58d1b70 (patch)
tree7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/ltac
parentb7a3c80754251c17bd2f266b00edb28e8a4e0c19 (diff)
[location] [travis] Add overlays for located_switch
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions