diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-10 18:33:58 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-06-10 18:33:58 +0200 |
commit | a0ad5ff6f9c7603610a7448935b36c9ed22c6435 (patch) | |
tree | 2ec8247b4ea1e10c781a2d13ed30b7a483380956 /riscV/Machregsaux.ml | |
parent | 9eccbd39710aab5d6bfe021c57f50a1916d37f70 (diff) | |
download | compcert-a0ad5ff6f9c7603610a7448935b36c9ed22c6435.tar.gz compcert-a0ad5ff6f9c7603610a7448935b36c9ed22c6435.zip |
x86 assembly: fix the comment delimiter for macos and make it per-OS
As reported in #399, it seems better to use `##` instead of `#` as
comment delimiter under macOS.
For the time being we keep using `#` for Linux and Cygwin.
Closes: #399
Diffstat (limited to 'riscV/Machregsaux.ml')
0 files changed, 0 insertions, 0 deletions