In_channel: Generate and shrink bytes only on length
#375
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Under some circumstances, `Sys.argv.(0)` is not pointing to the executable file, use `Sys.executable` instead (Circumstances: `dune exec ./test.exe` called in a subdirectory of the project)
In In_channel, bytes are used as input buffers so only their lengths is relevant: generate and shrink them by taking only their lengths into account
|
I triggered another round with getting a text file instead of the binary. |
Look for a text file to use to test `In_channel` to ensure that `input_line` and `input_all` will yield smaller results
|
I rebased to drop the two focusing commits and force-pushed the result. |
|
CI summary:
Since there were no |
This was referenced Aug 16, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR spawned out of #373.
In
In_channel,bytesare used as input buffers so only their lengths is relevant: generate and shrink them by taking only their lengths into accountIt currently contains a focusing commit to remove before merging, so I set this PR as a draft.