summaryrefslogtreecommitdiff
path: root/tools
Commit message (Expand)AuthorAgeFilesLines
* Merge commit 'c10217818f22d5eab897523a52a23fdf93c482f6' into parallel_minor_g...Tom Kelly2021-03-057-0/+21
|\
| * Inria CI: add timeouts to pipeline jobsSébastien Hinderer2020-09-167-0/+21
* | Merge commit 'd0e983e2aacfc77643f042a11673a7582bbb3015' into parallel_minor_g...Tom Kelly2021-03-056-0/+179
|\ \ | |/
| * Merge remote-tracking branch 'upstream/trunk' into trunkJohn Whitington2020-09-1115-124/+368
| |\
| * | Rename tools/unlabel --> tools/sync_stdlib_docsJohn Whitington2020-09-102-9/+9
| * | Remove SINCE work from tools/unlabelJohn Whitington2020-09-101-20/+6
| * | Restore tilde-removal, other little fixesJohn Whitington2020-08-051-1/+3
| * | Float.Array(Labels) generated by tools/unlabelJohn Whitington2020-08-051-0/+17
| * | Tildes back in ~random parameter in Hashtbl.createJohn Whitington2020-08-031-1/+1
| * | Remove unneeded comment, typoJohn Whitington2020-08-011-2/+2
| * | Fix label warningsJohn Whitington2020-07-311-1/+1
| * | Check-typo and indenting all doneJohn Whitington2020-07-311-4/+16
| * | More patch indentingJohn Whitington2020-07-311-2/+2
| * | Better indentation for moreLabels.mli patchesJohn Whitington2020-07-314-12/+12
| * | Better, simpler, removal of unix type aliasesJohn Whitington2020-07-301-53/+5
| * | Labeled and unlabeled @sinces automaticallyJohn Whitington2020-07-301-5/+19
| * | Tildes back in labeled modulesJohn Whitington2020-07-291-3/+3
| * | Tilde removal in place. Now will put them back in.John Whitington2020-07-291-46/+55
| * | Fix tools/unlabel to deal with Hashtbl injectivityJohn Whitington2020-07-271-1/+1
| * | Merge branch 'trunk' into trunkJohn Whitington2020-07-278-822/+14
| |\ \
| * | | Allow tools/unlabel to run from anywhereDavid Allsopp2020-07-271-39/+46
| * | | Check that tools/unlabel is a no-op in CIDavid Allsopp2020-07-271-0/+22
| * | | Match documentation and labelsJohn Whitington2020-07-191-1/+0
| * | | Generate moreLabels.mli programaticallyJohn Whitington2020-07-185-2/+53
| * | | Make hashtbl.mli / set.mli / map.mli from labeledJohn Whitington2020-07-181-0/+21
| * | | Check-typo fixJohn Whitington2020-07-181-1/+0
| * | | Unify unixLabels.mli / unix.mli via tools/unlabelJohn Whitington2020-07-171-1/+61
| * | | More check-typo fixesJohn Whitington2020-07-081-4/+8
| * | | Fixes per travis check-typo and travis changesJohn Whitington2020-07-081-2/+15
| * | | Unify labeled and unlabeled Standard Library modulesJohn Whitington2020-07-071-0/+11
* | | | Merge commit 'd9a3ad413f9567c418cf7809a110fac5fcd36f6c' into parallel_minor_g...Tom Kelly2021-03-0515-86/+344
|\ \ \ \ | | |_|/ | |/| |
| * | | Notify only on regressions for Inria CI's other-configs jobSébastien Hinderer2020-08-141-1/+1
| * | | Define Inria CI's other-configs job as a Jenkins pipeline, take #2Sébastien Hinderer2020-08-141-1/+1
| * | | Define Inria CI's other-configs job as a Jenkins pipeline, take #1Sébastien Hinderer2020-08-142-0/+43
| * | | Notify only on regressions for Inria CI's Risc-V jobSébastien Hinderer2020-08-131-1/+1
| * | | Define Inria CI's Risc-V job as a Jenkins pipeline, take #1Sébastien Hinderer2020-08-131-0/+42
| * | | Notify only on regressions for Inria CI's bootstrap jobSébastien Hinderer2020-08-131-1/+1
| * | | Use a pipeline to define the bootstrap Jenkins job, take #1Sébastien Hinderer2020-08-133-1/+44
| * | | Make the sanitizers and step-by-step-build CI jobs less verboseSébastien Hinderer2020-08-112-2/+2
| * | | tools/ci/inria/step-by-step-build/script: fixesSébastien Hinderer2020-08-111-2/+1
| * | | Split the extra-checks job, take #2Sébastien Hinderer2020-08-111-2/+3
| * | | Split Inria CI's extra-checks job, take #1Sébastien Hinderer2020-08-115-79/+114
| * | | dune-build: send e-mails only for regressionsSébastien Hinderer2020-08-111-1/+1
| * | | Always report failures of Inria CI's dune-build jobSébastien Hinderer2020-08-111-1/+1
| * | | tools/ci/inria/README.md: typographical improvementsSébastien Hinderer2020-08-111-2/+2
| * | | Inria CI: define the dune-build job as a Jenkins pipelineSébastien Hinderer2020-08-102-0/+41
| * | | Introduce the check-typo Jenkins pipelineSébastien Hinderer2020-08-103-6/+60
* | | | Merge commit '5da188b3ff468695681800b1a01191daef6dac0e' into parallel_minor_g...Tom Kelly2021-03-051-38/+24
|\ \ \ \ | |/ / /
| * | | Simplify the tools/ci/inria/extra-checks scriptSébastien Hinderer2020-08-061-34/+16
| * | | tools/ci/inria/extra-checks: stop mentionning the world targetSébastien Hinderer2020-08-031-1/+1