[server] cleaning usage of Json
Showing
- src/plugins/server/data.ml 22 additions, 24 deletionssrc/plugins/server/data.ml
- src/plugins/server/data.mli 2 additions, 2 deletionssrc/plugins/server/data.mli
- src/plugins/server/doc.ml 1 addition, 2 deletionssrc/plugins/server/doc.ml
- src/plugins/server/jbuffer.ml 1 addition, 1 deletionsrc/plugins/server/jbuffer.ml
- src/plugins/server/kernel_ast.ml 2 additions, 2 deletionssrc/plugins/server/kernel_ast.ml
- src/plugins/server/kernel_fc.ml 1 addition, 1 deletionsrc/plugins/server/kernel_fc.ml
- src/plugins/server/main.ml 0 additions, 1 deletionsrc/plugins/server/main.ml
- src/plugins/server/request.ml 4 additions, 6 deletionssrc/plugins/server/request.ml
- src/plugins/server/server_batch.ml 10 additions, 10 deletionssrc/plugins/server/server_batch.ml
Please register or sign in to comment