diff --git a/doc_src/history.txt b/doc_src/history.txt
index fc6dd13b4..7b00bea68 100644
--- a/doc_src/history.txt
+++ b/doc_src/history.txt
@@ -33,4 +33,4 @@ Interactively delete commands with prefix "foo".
 
 history --delete "foo"
 Delete command "foo" from history.
-<pre>
+</pre>