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 | |
| 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/
| -rw-r--r-- | lib/Commandline.ml (renamed from driver/Commandline.ml) | 0 | ||||
| -rw-r--r-- | lib/Commandline.mli (renamed from driver/Commandline.mli) | 0 |
2 files changed, 0 insertions, 0 deletions
diff --git a/driver/Commandline.ml b/lib/Commandline.ml index 672ed834..672ed834 100644 --- a/driver/Commandline.ml +++ b/lib/Commandline.ml diff --git a/driver/Commandline.mli b/lib/Commandline.mli index 8bb6f18f..8bb6f18f 100644 --- a/driver/Commandline.mli +++ b/lib/Commandline.mli |