summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorFreeyorp <TheFreeYorp+git@gmail.com>2024-06-04 14:16:59 +0000
committerFreeyorp <TheFreeYorp+git@gmail.com>2024-06-04 14:16:59 +0000
commit7c80d10503545cc870c084def44c0ea4a95fd290 (patch)
tree219cd96696e64f1dc04e483fb2ec2533d9e0d696 /tools
parent779beae0c495dc095808ea4015c5bfda6633e4f1 (diff)
downloadtmwa-7c80d10503545cc870c084def44c0ea4a95fd290.tar.gz
tmwa-7c80d10503545cc870c084def44c0ea4a95fd290.tar.bz2
tmwa-7c80d10503545cc870c084def44c0ea4a95fd290.tar.xz
tmwa-7c80d10503545cc870c084def44c0ea4a95fd290.zip
Rename .make to .mk
.mk is more widely understood than .make, for IDE usage.
Diffstat (limited to 'tools')
-rwxr-xr-xtools/protocol.py2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/protocol.py b/tools/protocol.py
index d63c22d..08c82b2 100755
--- a/tools/protocol.py
+++ b/tools/protocol.py
@@ -7124,7 +7124,7 @@ def make_dots(ctx):
#p = partition({k: ids_only(v.post) for (k, v) in d.items()})
if not os.path.exists('doc-gen'):
- # generate.make will succeed if missing the wiki repo
+ # generate.mk will succeed if missing the wiki repo
# but 'make doc' will fail
return
for g in glob.glob('doc-gen/*.gv'):