aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-06-23 17:08:38 +0200
committerMatthieu Sozeau2015-06-26 16:26:59 +0200
commita0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d (patch)
treecaed8f3c87d0aaab1ece708ef452094ae0353ce7 /dev
parentd9ac4c22a3a6543959d413120304e356d625c0f9 (diff)
Share prop/set values in sorts.ml.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions