diff options
| author | Carl Patenaude Poulin | 2017-11-11 15:45:58 -0500 |
|---|---|---|
| committer | GitHub | 2017-11-11 15:45:58 -0500 |
| commit | adbefdb8a9d9e7459630aa1808eae5b42cb3a6a5 (patch) | |
| tree | 65a99a66888c246fda2ba943389d0cc10dd13345 /stm/asyncTaskQueue.ml | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Single quotes break on Windows
As it is, running a `Makefile.coq` on Windows produces the following error:
`cut: ': No such file or directory`
Changing to double quotes fixes this.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions