summaryrefslogtreecommitdiff
path: root/library/states.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 11:58:21 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:27:32 +0200
commit1769cbaddea77112dd6f336316d8eb9a0945a1e6 (patch)
treeccd5b36d9d38daa85752c4e677614abc5eeab565 /library/states.ml
parent17b364613aa7bc04dfdac3efd47e4059afc3ac57 (diff)
Keep some file from doc/common/styles/html/simple
They are needed for HTML API doc generation.
Diffstat (limited to 'library/states.ml')
0 files changed, 0 insertions, 0 deletions