aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq.itarget
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-22 10:23:35 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-22 10:25:58 +0100
commit1abae19d5688b987b19efba8bcac8577892fcd27 (patch)
tree185481db06908e0f430ded68c12480f275c3476f /coq.itarget
parenta9f32885991263cf17093c6959732a339d473b45 (diff)
configure: improve last fix
Let's avoid the "if a=$(cmd ...)" since: - unless being a shell expert, it's not obvious it's testing the exit code of cmd. - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the exit code of cmd. Instead, we test the emptiness of the variable content afterwards
Diffstat (limited to 'coq.itarget')
0 files changed, 0 insertions, 0 deletions