aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-16 19:30:27 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-16 22:28:35 +0200
commit4158d921d506ce931ec940c55005f0698be9616b (patch)
treed7025e8bebddb0fe7308194ffeecd1940b362f30 /dev
parentd0da8a75cd1d600afa68da5e995d39a415234c2d (diff)
Revert "Naming main goal "Main""
(More thinking needed)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions