diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-10 10:12:41 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-11-10 10:12:41 +0100 |
| commit | 4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4 (patch) | |
| tree | b2551173c2f88d8c2e15cb30ed5978b008e6881c /ia32/ConstpropOpproof.v | |
| parent | 35e3f39bf967c4ed2ba3390b488604554306065d (diff) | |
| download | compcert-4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4.tar.gz compcert-4fad3b8da1227d4f5f7ff7d6cd2dbd2565d06ce4.zip | |
Harden Driver.command against EINTR errors
Sometimes, Unix.waitpid returns early with a EINTR error code, e.g. if a signal was handled. (Observed while running ccomp under the lldb debugger in MacOS X). Just restart Unix.waitpid in this case.
Diffstat (limited to 'ia32/ConstpropOpproof.v')
0 files changed, 0 insertions, 0 deletions