]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fbd42b0) | patch
* setprofileparam ==> setparam
authorLuca Padovani <luca.padovani@unito.it>
Mon, 24 May 2004 12:49:58 +0000 (12:49 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Mon, 24 May 2004 12:49:58 +0000 (12:49 +0000)
commitc6cb1f5a0ab5559e41eba001928e4a5ea595c051
tree57a691c56ef2b8b9e3c27e495b5ebd5c7d3efce3tree | snapshot
parentfbd42b06a420b96fe1f341b72156f05ede768032commit | diff
* setprofileparam ==> setparam
* serialization/deserialization of the profile file implemented (write-through
  semantics)
* cloning of a profile fixed
helm/uwobo/uwobo.ml diff | blob | history
helm/uwobo/uwobo_common.ml diff | blob | history
helm/uwobo/uwobo_profiles.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.