From d7cd9877804d760222d454d98922f1c2c9eddfe1 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:38:51 -0700 Subject: [PATCH] [sledge] Build: Do not clean help file Summary: The `sledge-help.txt` file is under source control, and should not be removed by `make clean`. Reviewed By: ngorogiannis Differential Revision: D23497893 fbshipit-source-id: 2061160a8 --- sledge/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sledge/dune b/sledge/dune index 215f47aae..db5206d00 100644 --- a/sledge/dune +++ b/sledge/dune @@ -138,4 +138,4 @@ (with-stdout-to sledge-help.txt (run tools/gen_help.sh))) - (mode promote-until-clean)) + (mode promote))