GitLab

Fix a compilation warning and update ML/.depend

See merge request !11

Fix a critical vulnerability of the corpus manager

See merge request !10

When the platform is installed in server mode, if the user edit the URL
in his browser's address bar, he can get writing permissions on the
corpus stored on the server.

Corpus manager

See merge request !9

The prefix of length n of the given list was returned in the reverse
order.

This is to avoid dependence problems when compiling the dictionary with
citation links.

* master:
  Web_corpus does no check and no exception mismatch

Conflicts:
	ML/web_corpus.ml
	ML/web_corpus.mli