diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-06-23 18:33:56 -0400 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-06-23 18:34:49 -0400 |
| commit | 9274e7448d85e682addb84440bded3800760ae14 (patch) | |
| tree | b6f3b56c85f596de7ac33926e747f555d8001ffe /coq/coq-par-compile.el | |
| parent | 3fb4147ad760df79d54ffa046ac94e6a5581daeb (diff) | |
Fix a typo
Diffstat (limited to 'coq/coq-par-compile.el')
| -rw-r--r-- | coq/coq-par-compile.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 25e82e2e..aac7447e 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -1053,7 +1053,7 @@ If the new job is a clone job, its state is a queue dependency QUEUE-DEP (which cannot be ready yet) - 'ready otherwise -If the new job is a 'file job it's state is 'enqueued-coqdep. If +If the new job is a 'file job its state is 'enqueued-coqdep. If there is space, coqdep is started immediately, otherwise the new job is put into the compilation queue. |