#include "MetricsInfo.h"
#include "OutputParams.h"
#include "output_xhtml.h"
+#include "texstream.h"
#include "frontends/Application.h"
#include "frontends/FontMetrics.h"
pi.pain.lines(xp, yp, 2, ColorName());
if (params_.kind == InsetSeparatorParams::PARBREAK) {
- yp[0] += 0.25 * asc * 0.75;
+ yp[0] += int(0.25 * asc * 0.75);
yp[1] = yp[0];
pi.pain.lines(xp, yp, 2, ColorName());
}