]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1c4fa3) | patch
New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Jun 2005 17:15:02 +0000 (17:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 Jun 2005 17:15:02 +0000 (17:15 +0000)
commite04169b2712f46b10e1923ff2fea5ebfd775c8dd
tree3ed07bf6cc1aeecde308d7d8453c8103ee01e637tree | snapshot
parentf1c4fa3d9ba8dcf53d78e0aee5464e9b82347ae7commit | diff
New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
 Pro:  no need of doing the weird "#use matitatop.bootstrap" by playing with
       ocaml internals.
 Pro:  local definitions and #opens in matitatop.bootstrap were lost. They are
       preserved in .ocamlinit.
 Cons: .ocamlinit must be in "." or in $HOME
 Cons: it can interfere with other .ocamlinit
helm/matita/.ocamlinit [new file with mode: 0644] blob
helm/matita/matitatop.bootstrap [deleted file] blob | history
helm/matita/matitatop.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.