aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 18:45:40 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-25 11:19:08 +0200
commitb6725a2d0077239e51385a62a526ab9465eea26d (patch)
tree7af2a0e3fe9b3a4c40b1e46de9e1211ec0e859cb /man
parent2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (diff)
The -compile option now accepts ".v" files and outputs a warning otherwise.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions