diff options
| author | Valentin Gagarin <valentin.gagarin@tweag.io> | 2023-03-03 12:56:23 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-03-03 12:56:23 +0100 |
| commit | e065131c1b9993bc086a71ce021d8e19afc492a0 (patch) | |
| tree | b9077c70e10c8438decbee0286c6959a38f3e019 /doc/manual | |
| parent | dd0aab2f94a6cef69d6219c3d363de76a11ed663 (diff) | |
cosmetic indentation
Co-authored-by: Théophane Hufschmitt <7226587+thufschmitt@users.noreply.github.com>
Diffstat (limited to 'doc/manual')
| -rw-r--r-- | doc/manual/local.mk | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual/local.mk b/doc/manual/local.mk index b6540e8e3..055882251 100644 --- a/doc/manual/local.mk +++ b/doc/manual/local.mk @@ -33,7 +33,7 @@ define process-includes matchline=$$(sed 's|/|\\/|g' <<< $$line); \ sed -i "/$$matchline/r $$(dirname $(2))/$$filename" $(2); \ sed -i "s/$$matchline//" $(2); \ - done < <(grep '{{#include' $(1)) + done < <(grep '{{#include' $(1)) endef $(d)/%.1: $(d)/src/command-ref/%.md |