On Friday, September 18, 2020 7:20:39 AM WEST Jürgen Spitzmüller wrote:
> Thanks from me, too.
>
> Jürgen
You are welcome. :-)
Actually I am confused why the code is needed at all.
What are the cases where we need to add a leftmost zero to a number? I could
understand if it was the first char in the string, and so position 0 and not
1.
On the other hand python understand that if a float number starts with a dot
then it is the same as if the 0 was there:
In [1]: .4*2
Out[1]: 0.8
Best regards,
--
José Abílio--
lyx-devel mailing list
lyx-devel@lists.lyx.org
http://lists.lyx.org/mailman/listinfo/lyx-devel
