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

Merge pull request #580 from ska80/ide-mode-socket-no-banner

Browse Source 
Suppress banner when running with --ide-mode-socket option
This commit is contained in:
Niklas Larsson 2020-08-20 11:07:35 +02:00 committed by GitHub
commit 8a346e18f2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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