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.cabal | |
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.cabal')
-rw-r--r-- | pancake.cabal | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pancake.cabal b/pancake.cabal index 47f7e02..1e41a36 100644 --- a/pancake.cabal +++ b/pancake.cabal @@ -51,6 +51,7 @@ executable pancake , process >= 1.6 && < 2 , terminfo >= 0.4.0.2 && < 1 , text >= 1.2.2.2 && < 2 + , unix >= 2.7.2.0 && < 3 , utf8-string >= 1.0.1.1 && < 2 , yaml >= 0.8.23.3 && < 1 -- hs-source-dirs: |