diff options
| author | Pierre-Marie Pédrot | 2017-02-01 10:52:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-01 10:54:53 +0100 |
| commit | c17c3faee20251cd5c7168246e9ffcd12d557f85 (patch) | |
| tree | 02635866b73d7595fad009cc17535a6bbf06c2fc /stm/asyncTaskQueue.ml | |
| parent | f86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff) | |
| parent | 568b38e1d599f8bac5adf140f5a114f2871bc436 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'stm/asyncTaskQueue.ml')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fa6422cdc5..8acc3c233a 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -170,7 +170,7 @@ module Make(T : Task) = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init 10 (fun _ -> + CList.init n (fun _ -> Universes.new_univ_level (Global.current_dirpath ())) in let rec kill_if () = |