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 /lib | |
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 'lib')
0 files changed, 0 insertions, 0 deletions