diff options
author | Charadon <dev@iotib.net> | 2022-10-08 14:57:05 -0400 |
---|---|---|
committer | Charadon <dev@iotib.net> | 2022-10-08 14:57:05 -0400 |
commit | 3ab7ec9bc605c34dc6ad5994457106b20b72d7ff (patch) | |
tree | 273cd7bf2a6ab4b979061620ac856631cdcaef69 | |
parent | defc744ef6bdbf6696336b790afbfe3082b97cfd (diff) | |
download | dscip-3ab7ec9bc605c34dc6ad5994457106b20b72d7ff.tar.gz |
Makefile: If makeinfo fails, try gmakeinfo instead.
-rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile index a62173a..b79001b 100644 --- a/Makefile +++ b/Makefile @@ -25,7 +25,7 @@ html: makeinfo --html manual.tex info: - makeinfo manual.tex + makeinfo manual.tex || gmakeinfo manual.tex uninstall: rm -rf $(SCRIPT_DIR)/../.. |