diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-03-20 11:11:24 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-03-20 11:11:24 +0100 |
| commit | 5bfa0059a144fb4333bbfecaa74690ba92a879ce (patch) | |
| tree | f79baab2043f0d4f9687a20d2afe51853f13acc7 /debug/DwarfPrinter.ml | |
| parent | a968152051941a0fc50a86c3fc15e90e22ed7c47 (diff) | |
| download | compcert-5bfa0059a144fb4333bbfecaa74690ba92a879ce.tar.gz compcert-5bfa0059a144fb4333bbfecaa74690ba92a879ce.zip | |
Quote directory for comp_dir entry.
The compilation directory entry needs quoting since it could be
a toplevel directory under windows.
Bug 21216
Diffstat (limited to 'debug/DwarfPrinter.ml')
0 files changed, 0 insertions, 0 deletions