Skip to content

Print output of some commands to stdout instead of stderr #12586

@punchagan

Description

@punchagan

While working on #12547, I learnt that Console.print prints to stderr by default. Unaware users of dune trying to pipe the output of dune through other shell tools like grep could trip up with this behavior. It could be useful to print the output from some commands to stdout, instead of stderr.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions