Skip to content

add ability to ignore unknown pipe names #1393#1394

Merged
gnodet merged 1 commit intojline:masterfrom
paulk-asert:ignore_unknown_pipes
Feb 11, 2026
Merged

add ability to ignore unknown pipe names #1393#1394
gnodet merged 1 commit intojline:masterfrom
paulk-asert:ignore_unknown_pipes

Conversation

@paulk-asert
Copy link
Copy Markdown
Contributor

This leaves the default the same but if the option is set to true, more friendly parsing ensues:

Screenshot 2025-08-14 at 4 21 17 pm

@gnodet gnodet added this to the 4.0.0 milestone Feb 11, 2026
@gnodet gnodet merged commit aae9f17 into jline:master Feb 11, 2026
9 checks passed
gnodet pushed a commit that referenced this pull request Feb 11, 2026
@gnodet
Copy link
Copy Markdown
Member

gnodet commented Feb 11, 2026

💚 All backports created successfully

Status Branch Result
jline-3.x

Questions ?

Please refer to the Backport tool documentation

gnodet pushed a commit that referenced this pull request Feb 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants