diff options
| author | Guillaume Melquiond | 2020-09-27 14:40:22 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-09-27 14:40:22 +0200 |
| commit | a5abb5d9c2d8c61be2444b5f5922cf124f98bae0 (patch) | |
| tree | 7c4d6ccf4bbc195264238cc77410965ee38487d8 /Makefile.dev | |
| parent | 27601f57d849757871af430b14efa379c7b84952 (diff) | |
Avoid lookup up too many characters.
This would cause issues in noninteractive mode. For example, when using
Drop, the first character of the OCaml code would be read by Coq's REPL
instead of OCaml's REPL.
The peek_string function is quite inefficient, since the Stream module
does not provide any good function to lookup arbitrary characters (or to
push back characters).
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions
