Skip to content

Commit b0efab6

Browse files
committed
fix: avoid coercion in macro
1 parent 586b723 commit b0efab6

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Cli/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1039,7 +1039,7 @@ section Macro
10391039
let mut shortName := quote (none : Option String)
10401040
let mut longName := flagName1
10411041
if let some flagName2 := flagName2 then
1042-
shortName := expandIdentLiterally flagName1
1042+
shortName ← `(some $(expandIdentLiterally flagName1))
10431043
longName := flagName2
10441044
let unitType : Term ← `(Unit)
10451045
let type :=

0 commit comments

Comments
 (0)