diff options
| author | gareuselesinge | 2012-01-26 10:33:16 +0000 |
|---|---|---|
| committer | gareuselesinge | 2012-01-26 10:33:16 +0000 |
| commit | 2e8c3911f22ccfec57f10ece68db731b4753d6c4 (patch) | |
| tree | 2b3aa6fb9989fc8b285ec908952c958126850521 /plugins/xml/doubleTypeInference.ml | |
| parent | 043669e582870be26eff682560187698bbc9e101 (diff) | |
Add support for plugin initialization function
Plugins can call add_known_plugin instead of add_known_module to
specify an initialization function. That function is granted to be
called after the system initialization (in case of static linking)
and every time their are "loaded" with Declare ML Module (even if the
.cmo or .cmxs is actually loaded only once since OCaml is unable to
unload dynamically linked modules).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14944 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/doubleTypeInference.ml')
0 files changed, 0 insertions, 0 deletions