diff options
Diffstat (limited to 'dev-ml/camlp4/files/reload.patch')
| -rw-r--r-- | dev-ml/camlp4/files/reload.patch | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/dev-ml/camlp4/files/reload.patch b/dev-ml/camlp4/files/reload.patch new file mode 100644 index 000000000000..8fbc1c05532c --- /dev/null +++ b/dev-ml/camlp4/files/reload.patch @@ -0,0 +1,13 @@ +Index: camlp4-4.08-1/camlp4/Camlp4/Struct/DynLoader.ml +=================================================================== +--- camlp4-4.08-1.orig/camlp4/Camlp4/Struct/DynLoader.ml ++++ camlp4-4.08-1/camlp4/Camlp4/Struct/DynLoader.ml +@@ -76,7 +76,7 @@ value load = + [ Not_found -> raise (Error file "file not found in path") ] + in + try Dynlink.loadfile fname with +- [ Dynlink.Error e -> raise (Error fname (Dynlink.error_message e)) ] ++ [ Dynlink.Error (Module_already_loaded _ ) -> () | Dynlink.Error e -> raise (Error fname (Dynlink.error_message e)) ] + }; + + |