diff options
| author | Michael Schmidt <github@mschmidt.me> | 2018-02-16 14:18:16 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2018-02-16 14:18:16 +0100 |
| commit | 95395781f2cc8ae8cd4e9a167795f594e3b6dc23 (patch) | |
| tree | 438d95d22ce144b77e8efa3988b9b255ea37f3b8 /configure | |
| parent | 16608ca8c91d51fb48a6a55f22d392420d727b63 (diff) | |
| download | compcert-95395781f2cc8ae8cd4e9a167795f594e3b6dc23.tar.gz compcert-95395781f2cc8ae8cd4e9a167795f594e3b6dc23.zip | |
Fix typo in comment
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -348,7 +348,7 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then fi # -# IA32 (64 bits) Target Configuration +# x86 (64 bits) Target Configuration # if test "$arch" = "x86" -a "$bitsize" = "64"; then |