diff options
author | 2017-02-14 11:36:04 +0100 | |
---|---|---|
committer | 2017-02-14 11:36:04 +0100 | |
commit | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (patch) | |
tree | 9f8bd1216d3943b2202804ab92334f11edf7df99 /vernac/metasyntax.mli | |
parent | b85742f187ec4d87733f88587534772502ad9a7d (diff) | |
parent | 7ce9edaeb49520990efb6785627cc1d6c80f7be6 (diff) |
Merge PR#253: Sort Search results by relevance
Diffstat (limited to 'vernac/metasyntax.mli')
0 files changed, 0 insertions, 0 deletions