diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-11 14:50:44 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-11 14:50:44 +0000 |
| commit | 3ab7a14bb005dae4141b434c1dd8ac73b4af2aa1 (patch) | |
| tree | 22283599628b301b7da2f29ee905db308e43dea0 /config | |
| parent | e685bc6f1bc8f7e1160cef53127a11d8d7be7306 (diff) | |
implements a better way to respect the Unix convention that processes receive their own name
as first argument. This is needed to make external tactics work when the external program
is interpreted and the operating system is Mac OS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10437 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions