#include "Exporter.h"
#include "Format.h"
#include "Mover.h"
+#include "texstream.h"
#include "frontends/alert.h"
size_t const pos = result.find("$$Contents(\"");
size_t const end = result.find("\")", pos);
- result.replace(pos, end + 2, contents);
+ result.replace(pos, end + 2- pos, contents);
}
return result;