[mlegendre]

And conversely, `/dev/stdout` (resp. `/dev/stderr`) is a convenient way to "redirect" output to stdout (resp stderr) instead of a file