aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-23 22:48:38 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-15 20:45:29 +0100
commit4db82417bdda1f9b0c7ea6ba9f6d71c03cc07eba (patch)
tree8973c496d28788486c50609492edb851d69ef036 /vernac
parent3d2680a97a1ab9d85c4672217ec7957ce390bca1 (diff)
[stm] Remove unused legacy stm interface.
Diffstat (limited to 'vernac')
0 files changed, 0 insertions, 0 deletions