[Server] use Filepath parameters for relevant options
Showing
- src/plugins/server/server_doc.ml 14 additions, 12 deletionssrc/plugins/server/server_doc.ml
- src/plugins/server/server_doc.mli 1 addition, 1 deletionsrc/plugins/server/server_doc.mli
- src/plugins/server/server_parameters.ml 3 additions, 2 deletionssrc/plugins/server/server_parameters.ml
- src/plugins/server/server_parameters.mli 1 addition, 1 deletionsrc/plugins/server/server_parameters.mli
Please register or sign in to comment