diff options
| author | defanor <defanor@uberspace.net> | 2017-11-16 03:17:28 +0300 |
|---|---|---|
| committer | defanor <defanor@uberspace.net> | 2017-11-16 03:17:28 +0300 |
| commit | 7390b37f0a907d764e0b183ca307f37c20bb068b (patch) | |
| tree | 2cbdb30a0ce809a724a1b9e2a1685b2a0e62e543 /Pancake/Command.hs | |
| parent | ca120bde0cf023219d765f06c3c52720ead9a6a6 (diff) | |
Handle SIGINT during getLine
It is too easy to kill pancake by accident, while trying to interrupt
a child process that finishes by itself right at that moment. So, only
quitting if there's two interruptions in a row (without any input
between them).
Minor refactoring has also happened in this commit.
Diffstat (limited to 'Pancake/Command.hs')
| -rw-r--r-- | Pancake/Command.hs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Pancake/Command.hs b/Pancake/Command.hs index 57b80c2..97cb25c 100644 --- a/Pancake/Command.hs +++ b/Pancake/Command.hs @@ -21,6 +21,7 @@ import Pancake.Configuration -- | Interactive user command. data Command = Quit + | Interrupt | Follow Int | More | GoTo (Maybe String) URI |