Browse Source

[display] avoid unnecessary string encoding

Jens Fischer 6 years ago
parent
commit
e3d7e7771a
1 changed files with 1 additions and 1 deletions
  1. 1 1
      src/context/display/displayJson.ml

+ 1 - 1
src/context/display/displayJson.ml

@@ -161,7 +161,7 @@ let handler =
 				DisplayToplevel.read_class_paths hctx.com ["init"];
 				let files = CompilationServer.get_files hctx.display#get_cs in
 				hctx.send_result (jobject [
-					"files", jstring (string_of_int (Hashtbl.length files))
+					"files", jint (Hashtbl.length files)
 				]);
 			)
 		);