diff options
| author | Gaëtan Gilbert | 2020-05-20 13:31:19 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-20 13:31:19 +0200 |
| commit | 547a384901d2785dcf9c849f09d4693174be3024 (patch) | |
| tree | 1cdf771d7765603cf4803be189ac74990a18b65a /plugins/syntax/float_syntax.ml | |
| parent | 2cd3c71ab3acf75a97e600feea9730461c08e0b8 (diff) | |
| parent | de90f071e088974a027c461fd5262387d246e80d (diff) | |
Merge PR #12342: Direct URL for triggering a pipeline with SKIP_DOCKER=false.
Reviewed-by: SkySkimmer
Ack-by: jfehrle
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions