From b4b66f6e2443cd05e163ac2577620ed06ea265e9 Mon Sep 17 00:00:00 2001
From: Camelid <camelidcamel@gmail.com>
Date: Sun, 6 Dec 2020 14:11:02 -0800
Subject: [PATCH] Fix trimming of lint docs

It was removing all the indentation before.

Co-authored-by: Eric Huss <eric@huss.org>
---
 src/tools/lint-docs/src/lib.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/tools/lint-docs/src/lib.rs b/src/tools/lint-docs/src/lib.rs
index 326b7948098..ea54a351e03 100644
--- a/src/tools/lint-docs/src/lib.rs
+++ b/src/tools/lint-docs/src/lib.rs
@@ -143,8 +143,8 @@ impl<'a> LintExtractor<'a> {
                     Some((lineno, line)) => {
                         let line = line.trim();
                         if let Some(text) = line.strip_prefix("/// ") {
-                            doc_lines.push(text.trim().to_string());
-                        } else if line.starts_with("///") {
+                            doc_lines.push(text.to_string());
+                        } else if line == "///" {
                             doc_lines.push("".to_string());
                         } else if line.starts_with("// ") {
                             // Ignore comments.