# HG changeset patch
# User wenzelm
# Date 1738844968 -3600
# Node ID a0b2cd020a8bec21137deecb8f9ff2f33b6e1ab4
# Parent  93195437fdee6f20885d3999a3f8ea785d3a0644
tuned comments;

diff -r 93195437fdee -r a0b2cd020a8b src/Pure/General/time.ML
--- a/src/Pure/General/time.ML	Thu Feb 06 12:46:13 2025 +0100
+++ b/src/Pure/General/time.ML	Thu Feb 06 13:29:28 2025 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/time.scala
     Author:     Makarius
 
-Time based on nanoseconds (idealized).
+Time based on nanoseconds (idealized), printed as milliseconds.
 *)
 
 signature TIME =