diff options
| author | Maxime Dénès | 2018-01-29 16:04:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-29 16:04:54 +0100 |
| commit | 4be607ec6c0b89e85566b4a6952bdf41e40fae7b (patch) | |
| tree | 8d1ab1f94ec3e434552fe6e4adc2c162c93a9764 /plugins/funind/glob_termops.ml | |
| parent | 60cb1f81e475d4b0f044a56ec4de503e42bad99a (diff) | |
Add test case for #5286.
Diffstat (limited to 'plugins/funind/glob_termops.ml')
0 files changed, 0 insertions, 0 deletions