From e8f36901235ae016aa0de869f2ba67722864dab6 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 28 Jan 2013 09:59:58 -0800
Subject: [PATCH] Change "// WARN" in tidy to "// NOTE" as requested by
 @catamorphism

---
 src/etc/tidy.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/etc/tidy.py b/src/etc/tidy.py
index 2eb32c100acd..65737c53e613 100644
--- a/src/etc/tidy.py
+++ b/src/etc/tidy.py
@@ -49,9 +49,9 @@ try:
                     report_err("FIXME without issue number")
             if line.find("TODO") != -1:
                 report_err("TODO is deprecated; use FIXME")
-            idx = line.find("// WARN")
+            idx = line.find("// NOTE")
             if idx != -1:
-                report_warn("WARN:" + line[idx + len("// WARN"):])
+                report_warn("NOTE:" + line[idx + len("// NOTE"):])
         if (line.find('\t') != -1 and
             fileinput.filename().find("Makefile") == -1):
             report_err("tab character")