fix: python time externs should return integers (#898)

aws · Oct 24, 2024 · 56b9b67 · 56b9b67
1 parent 736f831
commit 56b9b67
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/...ardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py b/...ardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py
@@ -8,10 +8,10 @@
 # Extend generated class with our externs
 class default__(smithy_dafny_standard_library.internaldafny.generated.Time.default__):
     def CurrentRelativeTimeMilli():
-        return datetime.datetime.now(tz = pytz.UTC).timestamp() * 1000
+        return round(datetime.datetime.now(tz = pytz.UTC).timestamp() * 1000)
 
     def CurrentRelativeTime():
-        return datetime.datetime.now(tz = pytz.UTC).timestamp()
+        return round(datetime.datetime.now(tz = pytz.UTC).timestamp())
 
     def GetCurrentTimeStamp():
         try:
@@ -22,4 +22,4 @@ def GetCurrentTimeStamp():
 
 
 # Export externs
-smithy_dafny_standard_library.internaldafny.generated.Time.default__ = default__
+smithy_dafny_standard_library.internaldafny.generated.Time.default__ = default__