From d9c113b5adec26f3c9e3a1abeda027ee00477b68 Mon Sep 17 00:00:00 2001 From: Christopher Lemmer Webber Date: Mon, 12 Jul 2021 10:24:46 -0400 Subject: [PATCH] Makefile: have "docs" subcommand write to correct subdirectory --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4f38c3b..881b6e3 100644 --- a/Makefile +++ b/Makefile @@ -15,4 +15,4 @@ clean: doc: docs docs: - scribble +m --htmls goblins/scribblings/goblins.scrbl + scribble --dest goblins/doc +m --htmls goblins/scribblings/goblins.scrbl