add soft spaces between groups of digits
This commit is contained in:
1 parent
a9b5848a5f
commit
c5e62b1614
1 file changed
+1
-1
@@ -196,7 +196,7 @@ lin pot5decimal d = {
|
||||
|
||||
oper
|
||||
spaceIf : DTail -> Str = \t -> case t of {
|
||||
T3 => SOFT_BIND ;
|
||||
T3 => SOFT_SPACE ;
|
||||
_ => BIND
|
||||
} ;
|
||||
|
||||
|
||||
Reference in new issue
Block a user