/* Set the pulse width of the specified channel in milliseconds.  */
void pwmout_pulsewidth_ms(pwmout_t *obj, int ms)
/* Set the pulse width of the specified channel in milliseconds.  */
void pwmout_pulsewidth_ms(pwmout_t *obj, int ms)
{
	pwmout_pulsewidth_us(obj, ms * 1000);
}