Add support for new tlapm command-line syntax#1085
Closed
glondu wants to merge 4 commits intotlaplus:masterfrom
Closed
Add support for new tlapm command-line syntax#1085glondu wants to merge 4 commits intotlaplus:masterfrom
glondu wants to merge 4 commits intotlaplus:masterfrom
Conversation
Member
|
Follow-up of tlaplus/tlapm#177 |
Calvin-L
reviewed
Nov 22, 2024
|
|
||
| command.add("--config"); | ||
|
|
||
| return (String[]) command.toArray(new String[command.size()]); |
Collaborator
There was a problem hiding this comment.
I don't think there's any need for an awkward array conversion here. It should be possible to simplify this to return command; if you make the method return List<String> instead of String[]. The only use of this method is as an argument to new ProcessBuilder, and that constructor can take either String[] or List<String>.
Author
There was a problem hiding this comment.
Right. I just reproduced the constructCommand pattern already present in the same file. I will push a simplified version.
542b618 to
c781c51
Compare
added 4 commits
November 25, 2024 08:53
Signed-off-by: Stephane Glondu <stephane.glondu@inria.fr>
Signed-off-by: Stephane Glondu <stephane.glondu@inria.fr>
…d `-d` Signed-off-by: Stephane Glondu <stephane.glondu@inria.fr>
Signed-off-by: Stephane Glondu <stephane.glondu@inria.fr>
c781c51 to
ea16f7a
Compare
Calvin-L
approved these changes
Dec 3, 2024
Member
|
IIRC, things changed over at the tlapm repo. What is the status of this PR? |
Contributor
|
This is no longer needed! |
This file contains hidden or 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
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.
No description provided.