diff options
Diffstat (limited to 'stdlib/sys.mli')
| -rw-r--r-- | stdlib/sys.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stdlib/sys.mli b/stdlib/sys.mli index 450327487..d316a6e0e 100644 --- a/stdlib/sys.mli +++ b/stdlib/sys.mli @@ -74,6 +74,7 @@ val sigtstp: int (* Interactive stop *) val sigttin: int (* Terminal read from background process *) val sigttou: int (* Terminal write from background process *) val sigvtalrm: int (* Timeout in virtual time *) +val sigprof: int (* Profiling interrupt *) (* Signal numbers for the standard POSIX signals. *) exception Break |