From 6b59bd86ca546895bf77dc60fcdd9ef54bf33a6c Mon Sep 17 00:00:00 2001 From: Gbkng Date: Thu, 14 Dec 2023 18:21:37 +0100 Subject: [PATCH] add a README for dev-tools directory --- dev-tools/README.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 dev-tools/README.md diff --git a/dev-tools/README.md b/dev-tools/README.md new file mode 100644 index 000000000..5630d40c0 --- /dev/null +++ b/dev-tools/README.md @@ -0,0 +1,7 @@ +This directory contains various tools for developers. + +# Format + +The `format` script format every C++ or Python in the current directory and its +subdirectories. See docstring header of `format` and `format --help` for more +information. -- 2.39.2