aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Letouzey2014-06-17 19:48:53 +0200
committerPierre Letouzey2014-06-17 19:48:53 +0200
commit3e5be89e137df93de6f13d7ea2270dd22b1d48d1 (patch)
tree71eaa17d522a8ce4187b9463796a43c127aa6d21 /dev
parentba4289e55b376074bd782f6dc376a76e7efaec11 (diff)
Dummy commit to test the new setup of coq-commits mailinglist
Diffstat (limited to 'dev')
-rw-r--r--dev/TODO1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/TODO b/dev/TODO
index 926861c965..605b28a7e2 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -1,4 +1,5 @@
+
o options de la ligne de commande
- reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml