diff options
author | 2014-07-10 15:49:03 +0200 | |
---|---|---|
committer | 2014-07-11 10:15:06 +0200 | |
commit | 31b99c5671c956de455372e43f935e1c70006f9d (patch) | |
tree | 2cdb46f8641b0ce89c8bb32284f7d459f13044dc /lib/feedback.mli | |
parent | 024c980ab64e0d1102a10fdd793339c1dc84ac0f (diff) |
Export type_of_global_ref (useful for external users of glob files)
Diffstat (limited to 'lib/feedback.mli')
0 files changed, 0 insertions, 0 deletions