idris-lang/Idris-dev — pull request #1176 by david-christiansen (2014-05-02 13:14:32+00:00)
Title: Allow the big startup banner to be disabled

This is done by adding `:set nobanner` to the init script.

Fixes #590.