diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-05-04 11:11:27 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-05-05 14:03:52 +0200 |
commit | 4a676623badb718da4055b7f26ee05f5097f4e7b (patch) | |
tree | 63ae1519f97355b928ded3eb1092d5bee83a6f42 /x86_64/Archi.v | |
parent | b46c0c01379da17dd96fc0cb8f0458100b7b1e5e (diff) | |
download | compcert-4a676623badb718da4055b7f26ee05f5097f4e7b.tar.gz compcert-4a676623badb718da4055b7f26ee05f5097f4e7b.zip |
Move Commandline to the lib/ directory
The Commandline module is reusable in other projects, and its license
(GPL) allows such reuse, so its natural place is in lib/ rather
than in driver/
Diffstat (limited to 'x86_64/Archi.v')
0 files changed, 0 insertions, 0 deletions