aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2021-03-27 17:00:16 +0100
committerEmilio Jesus Gallego Arias2021-03-29 22:27:43 +0200
commit7dba32f3204b85b0abf39161c7c8b7db4ce27247 (patch)
tree6855aebae5c615673787dcd4ed689b2fa03cf11a /dev
parentc6e9b36f2abc7bf434df8e9a6fea48ba9db4efc0 (diff)
[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0
Fixes #10704
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions