Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: isTty #3930

Merged
merged 2 commits into from
Apr 18, 2024
Merged

feat: isTty #3930

merged 2 commits into from
Apr 18, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Apr 17, 2024 •
edited
Loading

Adds IO.FS.Handle.isTty to check whether a handle is a Windows console or Unix terminal. Also adds an isTty field to IO.FS.Stream, so that this can be checked on, e.g., stdout.

@tydeu tydeu added the full-ci label Apr 17, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 17, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3930
419bb75
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#3930
23efef6
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Apr 17, 2024 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
28be5b2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
e8f865a
Kha
Kha reviewed Apr 17, 2024
View reviewed changes
src/runtime/io.cpp Outdated Show resolved Hide resolved
src/runtime/io.cpp Show resolved Hide resolved
src/Init/System/IO.lean Outdated Show resolved Hide resolved
@tydeu tydeu changed the title feat: isatty feat: isTty Apr 17, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
ba2a6af
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
6d4c9b4
@tydeu tydeu marked this pull request as ready for review April 17, 2024 21:14
@tydeu tydeu requested a review from joehendrix as a code owner April 17, 2024 21:14
@tydeu tydeu added the will-merge-soon …unless someone speaks up label Apr 17, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
3b08f24
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 17, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#3930
2f69406
@Kha Kha added this pull request to the merge queue Apr 18, 2024
Merged via the queue into leanprover:master with commit 0c9f9ab Apr 18, 2024
38 checks passed
@tydeu tydeu deleted the isatty branch April 18, 2024 14:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Kha left review comments

@joehendrix joehendrix Awaiting requested review from joehendrix

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tydeu @leanprover-community-mathlib4-bot @Kha