diff options
| author | Clément Pit-Claudel | 2020-03-26 16:39:36 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-26 16:39:36 -0400 |
| commit | 5f5f9520ccf0f107d381e5874a3743f47e37c409 (patch) | |
| tree | 2c6d2567c74a853cae8cf9f76f82f08140cc32e7 /dev/header.c | |
| parent | 3a34d96a9a8b570ca0c1e186d7c99683b3841e69 (diff) | |
| parent | 84ec585de78a961fe7a157cd9f34cd67be6af3ed (diff) | |
Merge PR #11929: Reintroduce a command that was actually used in another one. Fix build of PDF manual.
Reviewed-by: cpitclaudel
Diffstat (limited to 'dev/header.c')
0 files changed, 0 insertions, 0 deletions