name = name.replace(/\:/g, "_");
}
- var pretty = PrettyPrint.toPretty(File.read(sourceFile));
+ var pretty = imports.PrettyPrint.toPretty(File.read(sourceFile));
File.write(Options.target+"/symbols/src" + prettyfile,
'<html><head>' +
'<title>' + sourceFile + '</title>' +