]> matita.cs.unibo.it Git - helm.git/commit
1. helmns and domImpl moved to the misc module ;-(
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jan 2003 10:36:05 +0000 (10:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jan 2003 10:36:05 +0000 (10:36 +0000)
commit7fedf47037503b281d078eef6de13927020eb410
tree5016c294ff00681f8e349eea6652e48faaec3ea2
parent279178e6812c3fc9d376b5e3c919d59c486d6da3
1. helmns and domImpl moved to the misc module ;-(
2. all the constants and functions relative to stylesheet applications have
   been moved to the new module ApplyStylesheets, whose interface is really
   minimal.
helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/applyStylesheets.ml [new file with mode: 0644]
helm/gTopLevel/applyStylesheets.mli [new file with mode: 0644]
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/misc.ml
helm/gTopLevel/misc.mli