If I recall, converting between points and pixels isn't too difficult, if you make a kinda big assumption. If you make the assumption that the monitor is 96dpi, then the conversion is very easy. Points are computed as 72dpi where as on a typical Windows system, pixels are 96dpi. Therefore, to convert from pixels to points you do:
the_pixels * 72/96
or more simply
the_pixels * .75
But this has to be done as integer arithmetic, so to do it simply in mIRC:
alias px2pt {
return $int($calc($1 * .75))
}
If you test that formula, you will see that it works for the cases you provided
$px2pt(11) = 8
$px2pt(15) = 11
$px2pt(35) = 26
Like I said, that will work fine assuming the monitor is 96dpi.
