The JS backend "installs" highlight-hover.js

[nad]

When you compile using the JS backend the file highlight-hover.js is copied into the output directory. @ice1000, is this file used by the JS backend? I guess the answer is no. This can presumably be fixed by moving this file to its parent directory and removing "JS" </> from the following code:

agda/src/full/Agda/Interaction/Highlighting/HTML/Base.hs

Lines 204 to 205 in 9140409

	highlightJsFile <- getDataFileName $
	"JS" </> occurrenceHighlightJsFile

[ice1000]

I guess the answer is no.

You are right

[ice1000]

So the JS directory is for the JS backend only. I guess it's a good idea to document this behavior.

[nad]

So the JS directory is for the JS backend only.

Well, the JS backend copies everything from that directory into the target directory:

agda/src/full/Agda/Compiler/JS/Compiler.hs

Lines 158 to 162 in 54dfa72

	compDir <- compileDir
	liftIO $ do
	dataDir <- getDataDir
	let srcDir = dataDir </> "JS"
	copyDirContent srcDir compDir

I guess it's a good idea to document this behavior.

Perhaps a file with documentation could be put in the parent directory.