diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-01 09:51:11 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-01 09:51:11 +0000 |
| commit | 74a3cdbe96f9be6b74d18e00d59ee0f197b2a69c (patch) | |
| tree | 26119e89d64e7c83e0831106844b6a63bf3f1a1c /ide/ideutils.mli | |
| parent | 14efc1157cbcadfce5b1acc11bfba21a23fd08c8 (diff) | |
load_file takes advantage of same_file optimisation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14438 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
0 files changed, 0 insertions, 0 deletions