diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2017-10-24T09·00+0200 |
|---|---|---|
| committer | Eelco Dolstra <edolstra@gmail.com> | 2017-10-24T09·00+0200 |
| commit | 25f32625e2f2a3a1e1b3a3811da82f21c3a3b880 (patch) | |
| tree | 7538d1574f2a3fe30a68ff278975a271fd75c755 /doc/manual/style.css | |
| parent | af241ae7d3d2a9975d43c9137806a6ffcb96e95b (diff) | |
Remove the remote-builds option
This is superfluous since you can now just set "builders" to empty, e.g. "--builders ''".
Diffstat (limited to 'doc/manual/style.css')
0 files changed, 0 insertions, 0 deletions