aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching/ssrmatching.mli
diff options
context:
space:
mode:
authorGravatar Matej Košík <matej.kosik@inria.fr>2017-04-10 16:04:22 +0200
committerGravatar Matej Košík <matej.kosik@inria.fr>2017-04-10 16:04:22 +0200
commitcec95b3e62e973af5a6aa1cb571c3c4654c3005e (patch)
tree0994065d774a9bf8faf9280381aba4a6805d9cce /plugins/ssrmatching/ssrmatching.mli
parent69d0152e00c2a3c7341bef36dcb110a2c4263ccf (diff)
Revert "comment: typo"
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.mli')
0 files changed, 0 insertions, 0 deletions