diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-27 17:17:59 +0200 |
|---|---|---|
| committer |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-07-20 15:40:48 +0200 |
| commit | e61ccdcf8d30b2d9998ba4851ea7691114977b57 (patch) | |
| tree | c4a84fb5f9db7afcb76095bc8fd7acccb65128ad /intf/extend.ml | |
| parent | d70b9e9b901a836f80180200cfd591e05839ee28 (diff) | |
Remove trailing CR before diff in output and misc tests.
Diffstat (limited to 'intf/extend.ml')
0 files changed, 0 insertions, 0 deletions