When generating the HTML for the datagrid, we calculate starting widths

for all the columns, and turn some of those into floating point numbers

used for percentages. Those are then applied to a <col width="...%">.
The problem is that Django localizes numbers by default. Specifically,

the decimal point character. For some locales, including German, this

turns into a comma, giving us 100,0% instead of 100.0%.
We have a couple of options. One is to use |unlocalize to get the raw

value. The other is to use |stringformat to be precise about the

format we want the value in.
This change opts for |stringformat, so we can format this exactly for

the requirements in the tag. Going forward, we'll want to be sure we do

this any time we're dealing with numeric HTML attribute values that may

be localized (generally numbers with decimal places) that must be in a

specific format.

Tested with English and German locales. Verified that the datagrids

looked correct.
Checked the rest of Djblets's HTML for any similar width= attributes

that may also be impacted. Didn't find any (though it's possible this

problem is occurring in other forms).