aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-09-27 14:40:22 +0200
committerGuillaume Melquiond2020-09-27 14:40:22 +0200
commita5abb5d9c2d8c61be2444b5f5922cf124f98bae0 (patch)
tree7c4d6ccf4bbc195264238cc77410965ee38487d8 /Makefile.dev
parent27601f57d849757871af430b14efa379c7b84952 (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