diff options
| author | Théo Zimmermann | 2020-02-01 09:59:34 +0100 |
|---|---|---|
| committer | GitHub | 2020-02-01 09:59:34 +0100 |
| commit | 565645526215065fa3dbc5eee3100da158f463d1 (patch) | |
| tree | ef2c023e45d4e57cced7d89197acd8953d861ec9 /dev/ci | |
| parent | 37070565e8b7bead15f5abda2c409f1ad2348fa1 (diff) | |
No spaces with em-dashes.
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README-developers.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index dba3d38c6c..6a740b9033 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -43,7 +43,7 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab ### Breaking changes When your PR breaks an external project we test in our CI, you must -prepare a patch (or ask someone —possibly the project author— to +prepare a patch (or ask someone—possibly the project author—to prepare a patch) to fix the project. There is experimental support for an improved workflow, see [the next section](#experimental-automatic-overlay-creation-and-building), below |