From: Ben Pfaff <blp@cs.stanford.edu>
Date: Mon, 25 Feb 2019 17:47:21 +0000 (-0800)
Subject: doc: Time components may not actually be separated by ".".
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=640c9e545186880ad74c123b0ad5df347a9a3163;p=pspp

doc: Time components may not actually be separated by ".".

Reported by Matteo Ga.
---

diff --git a/doc/language.texi b/doc/language.texi
index fc459b6953..10fab4eca6 100644
--- a/doc/language.texi
+++ b/doc/language.texi
@@ -1182,7 +1182,7 @@ controls the character accepted and displayed as the decimal point
 For output, the date and time formats use the delimiters indicated in
 the table.  For input, date components may be separated by spaces or by
 one of the characters @samp{-}, @samp{/}, @samp{.}, or @samp{,}, and
-time components may be separated by spaces, @samp{:}, or @samp{.}.  On
+time components may be separated by spaces or @samp{:}.  On
 input, the @samp{Q} separating quarter from year and the @samp{WK}
 separating week from year may be uppercase or lowercase, and the spaces
 around them are optional.