diff options
| author | glondu | 2007-04-16 12:12:39 +0000 |
|---|---|---|
| committer | glondu | 2007-04-16 12:12:39 +0000 |
| commit | ed4fc9fbbf6b0bc2e43d8116e19e563741464dca (patch) | |
| tree | 3517f33a35c2c6fb23e9eada786360b31b5ba6ec /dev/include | |
| parent | 490fcaab846dc926c0945df6b0f8fb18c5bb0dd9 (diff) | |
Add the possibility to change the position of tabs in main window (from r9717).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9774 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions