aboutsummaryrefslogtreecommitdiff
path: root/library/goptions.ml
AgeCommit message (Expand)Author
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-15methode exportfilliatr
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Pathherbelin
1999-12-13 - méthode load sur les Hintsfilliatr
1999-12-05add_leaf -> application methode cachefilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-11-26module Goptions (etait Options)filliatr