idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity

Suppress banner when running with --ide-mode-socket option

Browse Source
This commit is contained in:
Kamil Shakirov 2020-08-20 14:18:12 +06:00
parent 310b7a007c
commit 899d425bbf
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/Idris/SetOptions.idr
View File

@ -52,6 +52,9 @@ preOptions (ExecFn _ :: opts)
preOptions (IdeMode :: opts)
= do setSession (record { nobanner = True } !getSession)
preOptions opts
preOptions (IdeModeSocket _ :: opts)
= do setSession (record { nobanner = True } !getSession)
preOptions opts
preOptions (CheckOnly :: opts)
= do setSession (record { nobanner = True } !getSession)
preOptions opts