Skip to content

Commit 56b9b67

Browse files
authored
fix: python time externs should return integers (#898)
1 parent 736f831 commit 56b9b67

File tree

1 file changed

+3
-3
lines changed
  • StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern

1 file changed

+3
-3
lines changed

StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/Time.py

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88
# Extend generated class with our externs
99
class default__(smithy_dafny_standard_library.internaldafny.generated.Time.default__):
1010
def CurrentRelativeTimeMilli():
11-
return datetime.datetime.now(tz = pytz.UTC).timestamp() * 1000
11+
return round(datetime.datetime.now(tz = pytz.UTC).timestamp() * 1000)
1212

1313
def CurrentRelativeTime():
14-
return datetime.datetime.now(tz = pytz.UTC).timestamp()
14+
return round(datetime.datetime.now(tz = pytz.UTC).timestamp())
1515

1616
def GetCurrentTimeStamp():
1717
try:
@@ -22,4 +22,4 @@ def GetCurrentTimeStamp():
2222

2323

2424
# Export externs
25-
smithy_dafny_standard_library.internaldafny.generated.Time.default__ = default__
25+
smithy_dafny_standard_library.internaldafny.generated.Time.default__ = default__

0 commit comments

Comments
 (0)