diff options
| author | Marc Glisse <marc.glisse@inria.fr> | 2020-04-20 22:16:54 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-20 22:16:54 +0200 |
| commit | 13963ade4135d47598843fb2f3ec196316200c28 (patch) | |
| tree | e99f425aa5e3bdad7b8e464be28ce586e0c37d92 /src/python/doc | |
| parent | 93cd1240ef65d8883ec624e6e393c09969bf4d6f (diff) | |
| parent | 70fb88a668c2cad837cbdea4863a136a1efc71c3 (diff) | |
Merge pull request #286 from mglisse/circleci
Tweak CircleCI parallelism
Diffstat (limited to 'src/python/doc')
0 files changed, 0 insertions, 0 deletions