diff options
author | Jason Gross <jgross@mit.edu> | 2017-08-24 15:50:51 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-08-24 15:50:51 -0400 |
commit | 7ac81ccfad04b1f0d3bad8f3b596e579b5f37224 (patch) | |
tree | 8abd4b8c4be2e8b44dc7315977544b348072793d /ide/coqide_ui.ml | |
parent | 85fdc6f58099d7bd605eb1f10d2a250a87e43771 (diff) |
Don't strip the newline, don't use \r
Not sure entirely what it was supposed to do, but stripping the newline
erased the following line
Diffstat (limited to 'ide/coqide_ui.ml')
0 files changed, 0 insertions, 0 deletions