diff options
| author | Peter Eisentraut | 2017-08-29 23:33:24 +0000 |
|---|---|---|
| committer | Peter Eisentraut | 2017-08-29 23:33:24 +0000 |
| commit | 00f6d5c2c3ae2f6d198e41800e5edcf0150d485b (patch) | |
| tree | 8e70ac00f2d2043bd65a0b8e68d8e36bb364cf4c /src/tools/git-external-diff | |
| parent | 6cbee65eee20c144bb4de169c6802f20e76785b0 (diff) | |
doc: Avoid sidebar element
The formatting of the sidebar element didn't carry over to the new tool
chain. Instead of inventing a whole new way of dealing with it, just
convert the one use to a "note".
Diffstat (limited to 'src/tools/git-external-diff')
0 files changed, 0 insertions, 0 deletions