- var src = {path: path, name:name, charset: IO.encoding, hilited: ""};
-
- if (JSDOC.hasOwnProperty('PluginManager')) {
- JSDOC.PluginManager.run("onPublishSrc", src);
- }
-
- if (src.hilited) {
- IO.saveFile(srcDir, name+publish.conf.ext, src.hilited);
- }
+ var pretty = PrettyPrint.toPretty(File.read(sourceFile));
+ File.write(Options.target+"/symbols/src" + prettyfile,
+ '<html><head>' +
+ '<title>' + files[i].substr(spath.length+1) + '</title>' +
+ '<link rel="stylesheet" type="text/css" href="../../../css/highlight-js.css"/>' +
+ '</head><body class="highlightpage">' +
+ pretty +
+ '</body></html>');