diff options
| author | Théo Zimmermann | 2019-08-22 19:06:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-22 19:06:32 +0200 |
| commit | 0fc73b31859abb42f3fccf018497b33dfa49c33b (patch) | |
| tree | dbbcfc278a2965f6aaf8e73aa1c765395f7c5e44 /doc/plugin_tutorial/tuto2/src/custom.mli | |
| parent | 45db028fa0ffbdd77cf87dc73f9d59d488e1c7b6 (diff) | |
[gitlab/ci] Do not wait for all builds to finish to run the tests.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/custom.mli')
0 files changed, 0 insertions, 0 deletions