/* Set the pulse width of the specified channel in seconds.  */
void pwmout_pulsewidth(pwmout_t *obj, float seconds)
/* Set the pulse width of the specified channel in seconds.  */
void pwmout_pulsewidth(pwmout_t *obj, float seconds)
{
	pwmout_pulsewidth_us(obj, (int)(seconds * 1000000.0f));
}