ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #2629 from melted/fix_completion

Browse Source 
Add desugarnats to completion
This commit is contained in:
Niklas Larsson 2015-09-18 00:45:32 +02:00
commit 9243fdfc42
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Idris/Completion.hs
View File

@ -87,6 +87,7 @@ completeOption = completeWord Nothing " \t" completeOpt
, "originalerrors" , "originalerrors"
, "autosolve" , "autosolve"
, "nobanner" , "nobanner"
, "desugarnats"
] ]
completeConsoleWidth :: CompletionFunc Idris completeConsoleWidth :: CompletionFunc Idris