diff options
| author | Benjamin Pierce <bcpierce00@users.noreply.github.com> | 2018-01-29 06:32:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-29 06:32:03 -0500 |
| commit | 557ecf86f3819d6274c7ba3d24e6a99a90f15882 (patch) | |
| tree | d8f0e5eef983c92db879676d32307eb0cf1f02c2 /src | |
| parent | 52e4ce07f438abde42b5ac508c10512446cc8f35 (diff) | |
| parent | a8802bd4ab067c5f936f998b1c29b5b985816d02 (diff) | |
| download | unison-557ecf86f3819d6274c7ba3d24e6a99a90f15882.zip unison-557ecf86f3819d6274c7ba3d24e6a99a90f15882.tar.gz unison-557ecf86f3819d6274c7ba3d24e6a99a90f15882.tar.bz2 | |
Merge pull request #139 from g-raud/eintr-stdin-read-restart
Uitext: reprint the whole prompt line when getInput fails with EINTR
Diffstat (limited to 'src')
| -rw-r--r-- | src/uitext.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/uitext.ml b/src/uitext.ml index d1a09a4..dac77e5 100644 --- a/src/uitext.ml +++ b/src/uitext.ml @@ -188,7 +188,7 @@ let rec selectAction batch actions tryagain = with (* Restart an interrupted system call (which can happen notably when * the process is put in the background by SIGTSTP). *) - Unix.Unix_error (Unix.EINTR, _, _) -> selectAction batch actions tryagain + Unix.Unix_error (Unix.EINTR, _, _) -> tryagainOrLoop() (* Simply print a slightly more informative message than the exception * itself (e.g. "Uncaught unix error: read failed: Resource temporarily * unavailable" or "Uncaught exception End_of_file"). *) |