aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-26 07:44:45 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-26 07:44:45 +0200
commitbeff9386b82c4aa6e066642d56a36c8034f54604 (patch)
treee71dc5490327b5b3fdbc69167aecab4ddaee2b7b /Makefile.common
parent8a235780d9b3612e1c01323398da3e80cbbf8e9f (diff)
Remove obsolete question about eta-conversion.
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions