diff options
author | 2017-10-06 12:37:15 +0200 | |
---|---|---|
committer | 2017-10-06 12:37:15 +0200 | |
commit | 3134ddd5dae8c9ab78a8aad181b2142f63907ecb (patch) | |
tree | d31ff1ae34bc0a8fd0608ad19d545c916d0d85db /lib/iStream.mli | |
parent | fb45ec112ebdf6f18143b844e317a555f14e3b74 (diff) | |
parent | 8fa1d224dafde29f5b527d380c069f196a042c60 (diff) |
Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.
Diffstat (limited to 'lib/iStream.mli')
0 files changed, 0 insertions, 0 deletions