{"thread":{"id":"37426","subject":"[RFC] improving advice message from \"git commit\" during a merge","startedAt":"2014-08-27T18:23:08Z","lastAt":"2014-08-29T06:44:09Z","messageCount":11,"participants":["Junio C Hamano","Jeff King","Matthieu Moy","Stefan Beller","Jonathan Nieder"],"isPatch":false,"patchVersion":null,"patchTotal":null},"messages":[{"id":"248422","messageId":"xmqq4mwxeqr7.fsf@gitster.dls.corp.google.com","threadId":"37426","inReplyTo":null,"subject":"[RFC] improving advice message from \"git commit\" during a merge","fromName":"Junio C Hamano","fromEmail":"gitster@pobox.com","sentAt":"2014-08-27T18:23:08Z","receivedAt":"2014-08-27T18:23:08Z","isPatch":false,"sender":{"key":"gitster@pobox.com","avatar":"https://avatars.githubusercontent.com/u/54884?v=4"},"body":"When there are unmerged paths, you would often get something like\nthis:\n\n [git.git (pu|MERGING]$ git commit\n U copy.c\n U wrapper.c\n error: commit is not possible because you have unmerged files.\n hint: Fix them up in the work tree, and then use 'git add/rm '\n hint: as appropriate to mark resolution and make a commit, or use\n hint: 'git commit -a'.\n fatal: Exiting because of an unresolved conflict.\n\nwhich is all good and correct, but I am wondering if we can be a bit\nmore helpful by customizing the message in various ways.\n\n - When all the unmerged paths have their conflicts resolved in the\n working tree, we do not have to say \"Fix them up in the work\n tree,\". We can instead say \"You seem to have fixed them up in\n the work tree already,\" or something.\n\n - When some of the unmerged paths have their conflicts still in the\n working tree, we can name them separately from the ones that have\n already been dealt with.\n\n U copy.c\n U wrapper.c (conflicts already resolved in the working tree)\n\n - Hasty-and-careless new users will be incorrectly enticed to type\n the command given by \"or use 'git commit -a'\" at the end of this\n advice message without thinking. Perhaps it is safer to stop the\n sentence at \"... and make a commit.\" and drop that last bit while\n there are conflicts still in the working tree files. We should\n use the current end-of-message only when all the conflicts have\n been resolved in the working tree.\n\n - The \"/rm\" in \"use 'git add/rm '\" is often useless, as it is\n much rarer to remove a path than adding one. Perhaps show that\n part only when there is a conflicted path with stage #2 but not\n stage #3 (i.e. they kept what we removed) or vice versa. \"add\"\n needs to stay there no matter what, as that is how we tell the\n index \"this is the final content\".\n\nI am not doing this myself soon, though. Hint, hint...\n"},{"id":"248426","messageId":"20140827191857.GB7561@peff.net","threadId":"37426","inReplyTo":"xmqq4mwxeqr7.fsf@gitster.dls.corp.google.com","subject":"Re: [RFC] improving advice message from \"git commit\" during a merge","fromName":"Jeff King","fromEmail":"peff@peff.net","sentAt":"2014-08-27T19:18:58Z","receivedAt":"2014-08-27T19:18:58Z","isPatch":false,"sender":{"key":"peff@peff.net","avatar":"https://avatars.githubusercontent.com/u/45925?v=4"},"body":"On Wed, Aug 27, 2014 at 11:23:08AM -0700, Junio C Hamano wrote:\n\n> When there are unmerged paths, you would often get something like\n> this:\n> \n> [git.git (pu|MERGING]$ git commit\n> U copy.c\n> U wrapper.c\n> error: commit is not possible because you have unmerged files.\n> hint: Fix them up in the work tree, and then use 'git add/rm '\n> hint: as appropriate to mark resolution and make a commit, or use\n> hint: 'git commit -a'.\n> fatal: Exiting because of an unresolved conflict.\n> \n> which is all good and correct, but I am wondering if we can be a bit\n> more helpful by customizing the message in various ways.\n> \n> - When all the unmerged paths have their conflicts resolved in the\n> working tree, we do not have to say \"Fix them up in the work\n> tree,\". We can instead say \"You seem to have fixed them up in\n> the work tree already,\" or something.\n\nHow are you determining what has been resolved? By looking for \"<<<<<<<\"\nmarkers? That feels a little flaky, but I guess it would probably work\nwell enough in practice.\n\nIf we started using that heuristic, it would probably make sense to\nteach \"git status\" about it (and then maybe just have a failed \"commit\"\nrely on wt_status to produce the output).\n\n> I am not doing this myself soon, though. Hint, hint...\n\nMe either, though it all seems like a sensible direction to me.\n\n-Peff\n"},{"id":"248428","messageId":"xmqqmwapd96c.fsf@gitster.dls.corp.google.com","threadId":"37426","inReplyTo":"20140827191857.GB7561@peff.net","subject":"Re: [RFC] improving advice message from \"git commit\" during a merge","fromName":"Junio C Hamano","fromEmail":"gitster@pobox.com","sentAt":"2014-08-27T19:28:11Z","receivedAt":"2014-08-27T19:28:11Z","isPatch":false,"sender":{"key":"gitster@pobox.com","avatar":"https://avatars.githubusercontent.com/u/54884?v=4"},"body":"Jeff King writes:\n\n>> - When all the unmerged paths have their conflicts resolved in the\n>> working tree, we do not have to say \"Fix them up in the work\n>> tree,\". We can instead say \"You seem to have fixed them up in\n>> the work tree already,\" or something.\n>\n> How are you determining what has been resolved? By looking for \"<<<<<<<\"\n> markers? That feels a little flaky, but I guess it would probably work\n> well enough in practice.\n\nI was going to say \"whatever rerere does\" by reusing whatever it has\nalready implemented.\n\n> If we started using that heuristic, it would probably make sense to\n> teach \"git status\" about it (and then maybe just have a failed \"commit\"\n> rely on wt_status to produce the output).\n>\n>> I am not doing this myself soon, though. Hint, hint...\n>\n> Me either, though it all seems like a sensible direction to me.\n"},{"id":"248476","messageId":"1409219218-9475-1-git-send-email-Matthieu.Moy@imag.fr","threadId":"37426","inReplyTo":"xmqq4mwxeqr7.fsf@gitster.dls.corp.google.com","subject":"[PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Matthieu Moy","fromEmail":"matthieu.moy@imag.fr","sentAt":"2014-08-28T09:46:58Z","receivedAt":"2014-08-28T09:46:58Z","isPatch":true,"sender":{"key":"git@matthieu-moy.fr","avatar":"https://avatars.githubusercontent.com/u/14709?v=4"},"body":"'git commit -a' is rarely a good way to mark conflicts as resolved: the\nuser anyway has to go manually through the list of conflicts to do the\nactual resolution, and it is usually better to use \"git add\" on each\nfiles after doing the resolution.\n\nOn the other hand, using 'git commit -a' is potentially dangerous, as it\nmakes it very easy to mistakenly commit conflict markers without\nnoticing.\n\nWhile we're there, synchronize the 'git pull' and 'git merge' messages:\nthe first was ending with '... and make a commit.', but not the later.\n\nSigned-off-by: Matthieu Moy \n---\n> - Hasty-and-careless new users will be incorrectly enticed to type\n> the command given by \"or use 'git commit -a'\" at the end of this\n> advice message without thinking. Perhaps it is safer to stop the\n> sentence at \"... and make a commit.\" and drop that last bit while\n> there are conflicts still in the working tree files. We should\n> use the current end-of-message only when all the conflicts have\n> been resolved in the working tree.\n\nIt was already on my todo-list, as a friend of mine semi-beginner with\nGit complained about the mis-advice the other day, and I had to agree.\n\nEventually, git could detect that conflicts have been resolved, but\nthen that would be a different message, as not only \"use git commit\n-a\" could be resurected, but \"Fix them up in the work tree\" should be\ndropped when it is the case.\n\n> I am not doing this myself soon, though. Hint, hint...\n\nI guess I'm just taking the low hanging fruit here ;-).\n\n advice.c | 3 +--\n git-pull.sh | 2 +-\n 2 files changed, 2 insertions(+), 3 deletions(-)\n\ndiff --git a/advice.c b/advice.c\nindex 9b42033..3b8bf3c 100644\n--- a/advice.c\n+++ b/advice.c\n@@ -86,8 +86,7 @@ int error_resolve_conflict(const char *me)\n \t\t * other commands doing a merge do.\n \t\t */\n \t\tadvise(_(\"Fix them up in the work tree, and then use 'git add/rm '\\n\"\n-\t\t\t \"as appropriate to mark resolution and make a commit, or use\\n\"\n-\t\t\t \"'git commit -a'.\"));\n+\t\t\t \"as appropriate to mark resolution and make a commit.\"));\n \treturn -1;\n }\n \ndiff --git a/git-pull.sh b/git-pull.sh\nindex 18a394f..4d4fc77 100755\n--- a/git-pull.sh\n+++ b/git-pull.sh\n@@ -20,7 +20,7 @@ die_conflict () {\n if [ $(git config --bool --get advice.resolveConflict || echo true) = \"true\" ]; then\n \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\n Please, fix them up in the work tree, and then use 'git add/rm '\n-as appropriate to mark resolution, or use 'git commit -a'.\")\"\n+as appropriate to mark resolution and make a commit.\")\"\n else\n \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\")\"\n fi\n-- \n2.0.2.737.gfb43bde\n"},{"id":"248479","messageId":"53FF1DEE.8030504@gmail.com","threadId":"37426","inReplyTo":"xmqq4mwxeqr7.fsf@gitster.dls.corp.google.com","subject":"Re: [RFC] improving advice message from \"git commit\" during a merge","fromName":"Stefan Beller","fromEmail":"stefanbeller@gmail.com","sentAt":"2014-08-28T12:17:50Z","receivedAt":"2014-08-28T12:17:50Z","isPatch":false,"sender":{"key":"stefanbeller@gmail.com","avatar":"https://avatars.githubusercontent.com/u/455868?v=4"},"body":"On 27.08.2014 20:23, Junio C Hamano wrote:\n> I am not doing this myself soon, though. Hint, hint...\n\nI asked once upon a time, if there was a place, \nwhich collects such topics for casual contributors and new comers.\n\nWould you mind to update the leftover bits at\nhttp://git-blame.blogspot.de/search?q=leftover&by-date=true\n?\n\nThanks,\nStefan\n"},{"id":"248501","messageId":"xmqqoav4bkum.fsf@gitster.dls.corp.google.com","threadId":"37426","inReplyTo":"53FF1DEE.8030504@gmail.com","subject":"Re: [RFC] improving advice message from \"git commit\" during a merge","fromName":"Junio C Hamano","fromEmail":"gitster@pobox.com","sentAt":"2014-08-28T17:11:13Z","receivedAt":"2014-08-28T17:11:13Z","isPatch":false,"sender":{"key":"gitster@pobox.com","avatar":"https://avatars.githubusercontent.com/u/54884?v=4"},"body":"Stefan Beller writes:\n\n> On 27.08.2014 20:23, Junio C Hamano wrote:\n>> I am not doing this myself soon, though. Hint, hint...\n>\n> I asked once upon a time, if there was a place, \n> which collects such topics for casual contributors and new comers.\n>\n> Would you mind to update the leftover bits at\n> http://git-blame.blogspot.de/search?q=leftover&by-date=true\n> ?\n\nThey live in a bit more permanent home at\n\n http://git-blame.blogspot.com/p/leftover-bits.html\n\nthese days.\n\nIt is too early to tell this particular one will make an entry there\nyet ;-)\n"},{"id":"248504","messageId":"xmqqa96obk1e.fsf@gitster.dls.corp.google.com","threadId":"37426","inReplyTo":"1409219218-9475-1-git-send-email-Matthieu.Moy@imag.fr","subject":"Re: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Junio C Hamano","fromEmail":"gitster@pobox.com","sentAt":"2014-08-28T17:28:45Z","receivedAt":"2014-08-28T17:28:45Z","isPatch":true,"sender":{"key":"gitster@pobox.com","avatar":"https://avatars.githubusercontent.com/u/54884?v=4"},"body":"Matthieu Moy writes:\n\n> 'git commit -a' is rarely a good way to mark conflicts as resolved: the\n> user anyway has to go manually through the list of conflicts to do the\n> actual resolution, and it is usually better to use \"git add\" on each\n> files after doing the resolution.\n>\n> On the other hand, using 'git commit -a' is potentially dangerous, as it\n> makes it very easy to mistakenly commit conflict markers without\n> noticing.\n>\n> While we're there, synchronize the 'git pull' and 'git merge' messages:\n> the first was ending with '... and make a commit.', but not the later.\n>\n> Signed-off-by: Matthieu Moy \n> ---\n>> - Hasty-and-careless new users will be incorrectly enticed to type\n>> the command given by \"or use 'git commit -a'\" at the end of this\n>> advice message without thinking. Perhaps it is safer to stop the\n>> sentence at \"... and make a commit.\" and drop that last bit while\n>> there are conflicts still in the working tree files. We should\n>> use the current end-of-message only when all the conflicts have\n>> been resolved in the working tree.\n>\n> It was already on my todo-list, as a friend of mine semi-beginner with\n> Git complained about the mis-advice the other day, and I had to agree.\n\n\n\n> Eventually, git could detect that conflicts have been resolved, but\n> then that would be a different message, as not only \"use git commit\n> -a\" could be resurected, but \"Fix them up in the work tree\" should be\n> dropped when it is the case.\n\nThis paragraph should be in the log message, shouldn't it, probably\nwith s/could/should/?\n\n> I guess I'm just taking the low hanging fruit here ;-).\n\nI'd say it is more like scooping a fruit lying on the ground before\nit rots, but thanks anyway ;-)\n\n> advice.c | 3 +--\n> git-pull.sh | 2 +-\n> 2 files changed, 2 insertions(+), 3 deletions(-)\n>\n> diff --git a/advice.c b/advice.c\n> index 9b42033..3b8bf3c 100644\n> --- a/advice.c\n> +++ b/advice.c\n> @@ -86,8 +86,7 @@ int error_resolve_conflict(const char *me)\n> \t\t * other commands doing a merge do.\n> \t\t */\n> \t\tadvise(_(\"Fix them up in the work tree, and then use 'git add/rm '\\n\"\n> -\t\t\t \"as appropriate to mark resolution and make a commit, or use\\n\"\n> -\t\t\t \"'git commit -a'.\"));\n> +\t\t\t \"as appropriate to mark resolution and make a commit.\"));\n> \treturn -1;\n> }\n> \n> diff --git a/git-pull.sh b/git-pull.sh\n> index 18a394f..4d4fc77 100755\n> --- a/git-pull.sh\n> +++ b/git-pull.sh\n> @@ -20,7 +20,7 @@ die_conflict () {\n> if [ $(git config --bool --get advice.resolveConflict || echo true) = \"true\" ]; then\n> \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\n> Please, fix them up in the work tree, and then use 'git add/rm '\n> -as appropriate to mark resolution, or use 'git commit -a'.\")\"\n> +as appropriate to mark resolution and make a commit.\")\"\n> else\n> \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\")\"\n> fi\n"},{"id":"248505","messageId":"vpq8um8v7dz.fsf@anie.imag.fr","threadId":"37426","inReplyTo":"xmqqa96obk1e.fsf@gitster.dls.corp.google.com","subject":"Re: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Matthieu Moy","fromEmail":"matthieu.moy@grenoble-inp.fr","sentAt":"2014-08-28T17:41:44Z","receivedAt":"2014-08-28T17:41:44Z","isPatch":true,"sender":{"key":"matthieu.moy@grenoble-inp.fr","avatar":"https://gravatar.com/avatar/72c8a2705971a25dfaff23cece15130d405685845d911aedd5667ace277f3fc5?d=mp&s=160"},"body":"Junio C Hamano writes:\n\n> Matthieu Moy writes:\n>\n>> 'git commit -a' is rarely a good way to mark conflicts as resolved: the\n>> user anyway has to go manually through the list of conflicts to do the\n>> actual resolution, and it is usually better to use \"git add\" on each\n>> files after doing the resolution.\n>>\n>> On the other hand, using 'git commit -a' is potentially dangerous, as it\n>> makes it very easy to mistakenly commit conflict markers without\n>> noticing.\n>>\n>> While we're there, synchronize the 'git pull' and 'git merge' messages:\n>> the first was ending with '... and make a commit.', but not the later.\n>>\n>> Signed-off-by: Matthieu Moy \n>> ---\n>>> - Hasty-and-careless new users will be incorrectly enticed to type\n>>> the command given by \"or use 'git commit -a'\" at the end of this\n>>> advice message without thinking. Perhaps it is safer to stop the\n>>> sentence at \"... and make a commit.\" and drop that last bit while\n>>> there are conflicts still in the working tree files. We should\n>>> use the current end-of-message only when all the conflicts have\n>>> been resolved in the working tree.\n>>\n>> It was already on my todo-list, as a friend of mine semi-beginner with\n>> Git complained about the mis-advice the other day, and I had to agree.\n>\n>\n>\n>> Eventually, git could detect that conflicts have been resolved, but\n>> then that would be a different message, as not only \"use git commit\n>> -a\" could be resurected, but \"Fix them up in the work tree\" should be\n>> dropped when it is the case.\n>\n> This paragraph should be in the log message, shouldn't it, probably\n> with s/could/should/?\n\nI think the commit message explains well enough why the change is good.\nThe additional paragraph explains why I did not do it the way your\nmessage suggests (which has to do with the current discussion, but does\nnot have to be recorded in history IHMO).\n\n-- \nMatthieu Moy\nhttp://www-verimag.imag.fr/~moy/\n"},{"id":"248509","messageId":"20140828181638.GB20185@google.com","threadId":"37426","inReplyTo":"1409219218-9475-1-git-send-email-Matthieu.Moy@imag.fr","subject":"Re: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Jonathan Nieder","fromEmail":"jrnieder@gmail.com","sentAt":"2014-08-28T18:16:38Z","receivedAt":"2014-08-28T18:16:38Z","isPatch":true,"sender":{"key":"jrnieder@gmail.com","avatar":"https://avatars.githubusercontent.com/u/281595?v=4"},"body":"Matthieu Moy wrote:\n\n> Signed-off-by: Matthieu Moy \n[...]\n> ---\n> advice.c | 3 +--\n> git-pull.sh | 2 +-\n> 2 files changed, 2 insertions(+), 3 deletions(-)\n\nThanks for taking it on.\n\nReviewed-by: Jonathan Nieder \n\n[...]\n> It was already on my todo-list, as a friend of mine semi-beginner with\n> Git complained about the mis-advice the other day, and I had to agree.\n\nThat's a useful sort of thing to put in a commit message. :)\n\n> Eventually, git could detect that conflicts have been resolved, but\n> then that would be a different message, as not only \"use git commit\n> -a\" could be resurected, but \"Fix them up in the work tree\" should be\n> dropped when it is the case.\n\nAs is this --- when I wonder why code isn't a certain way, ideas for\nfuture work found in the description for the blamed commit are often\nhelpful in explaining the current state and saving me from blind\nalleys in changing it.\n\nAnyway, this is already a very good change as-is.\n\nActually, I'd be nervous about suggesting \"use git commit -a\" without\nat least also saying \"inspect the result or run tests\" in the\nno-conflict-markers-found case. Rerere sometimes makes mistakes, and\nthe result of picking one side when merging binary files can be even\nworse.\n\nThanks,\nJonathan\n"},{"id":"248511","messageId":"xmqqppfka2bb.fsf@gitster.dls.corp.google.com","threadId":"37426","inReplyTo":"20140828181638.GB20185@google.com","subject":"Re: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Junio C Hamano","fromEmail":"gitster@pobox.com","sentAt":"2014-08-28T18:36:56Z","receivedAt":"2014-08-28T18:36:56Z","isPatch":true,"sender":{"key":"gitster@pobox.com","avatar":"https://avatars.githubusercontent.com/u/54884?v=4"},"body":"Jonathan Nieder writes:\n\n>> It was already on my todo-list, as a friend of mine semi-beginner with\n>> Git complained about the mis-advice the other day, and I had to agree.\n>\n> That's a useful sort of thing to put in a commit message. :)\n>\n>> Eventually, git could detect that conflicts have been resolved, but\n>> then that would be a different message, as not only \"use git commit\n>> -a\" could be resurected, but \"Fix them up in the work tree\" should be\n>> dropped when it is the case.\n>\n> As is this --- when I wonder why code isn't a certain way, ideas for\n> future work found in the description for the blamed commit are often\n> helpful in explaining the current state and saving me from blind\n> alleys in changing it.\n\nYes.\n\n> Anyway, this is already a very good change as-is.\n>\n> Actually, I'd be nervous about suggesting \"use git commit -a\" without\n> at least also saying \"inspect the result or run tests\" in the\n> no-conflict-markers-found case. Rerere sometimes makes mistakes, and\n> the result of picking one side when merging binary files can be even\n> worse.\n\nHere is how I phrased in the one queued tentatively.\n\n-- >8 --\nFrom: Matthieu Moy \nDate: Thu, 28 Aug 2014 11:46:58 +0200\nSubject: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict\n\n'git commit -a' is rarely a good way to mark conflicts as resolved:\nthe user anyway has to go manually through the list of conflicts to\ndo the actual resolution, and it is usually better to use \"git add\"\non each files after doing the resolution.\n\nOn the other hand, using 'git commit -a' is potentially dangerous,\nas it makes it very easy to mistakenly commit conflict markers\nwithout noticing, and even worse, the user may have started a merge\nwhile having local changes that do not overlap with it in the\nworking tree.\n\nWhile we're there, synchronize the 'git pull' and 'git merge'\nmessages: the first was ending with '... and make a commit.', but\nnot the latter.\n\nEventually, git should detect that conflicts have been resolved in\nthe working tree and tailor these messages further. Not only \"use\ngit commit -a\" could be resurected, but \"Fix them up in the work\ntree\" should be dropped when it happens.\n\nSigned-off-by: Matthieu Moy \nSigned-off-by: Junio C Hamano \n\ndiff --git a/advice.c b/advice.c\nindex 9b42033..3b8bf3c 100644\n--- a/advice.c\n+++ b/advice.c\n@@ -86,8 +86,7 @@ int error_resolve_conflict(const char *me)\n \t\t * other commands doing a merge do.\n \t\t */\n \t\tadvise(_(\"Fix them up in the work tree, and then use 'git add/rm '\\n\"\n-\t\t\t \"as appropriate to mark resolution and make a commit, or use\\n\"\n-\t\t\t \"'git commit -a'.\"));\n+\t\t\t \"as appropriate to mark resolution and make a commit.\"));\n \treturn -1;\n }\n \ndiff --git a/git-pull.sh b/git-pull.sh\nindex 18a394f..4d4fc77 100755\n--- a/git-pull.sh\n+++ b/git-pull.sh\n@@ -20,7 +20,7 @@ die_conflict () {\n if [ $(git config --bool --get advice.resolveConflict || echo true) = \"true\" ]; then\n \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\n Please, fix them up in the work tree, and then use 'git add/rm '\n-as appropriate to mark resolution, or use 'git commit -a'.\")\"\n+as appropriate to mark resolution and make a commit.\")\"\n else\n \tdie \"$(gettext \"Pull is not possible because you have unmerged files.\")\"\n fi\n"},{"id":"248536","messageId":"vpqegvzu75y.fsf@anie.imag.fr","threadId":"37426","inReplyTo":"xmqqppfka2bb.fsf@gitster.dls.corp.google.com","subject":"Re: [PATCH] merge, pull: stop advising 'commit -a' in case of conflict","fromName":"Matthieu Moy","fromEmail":"matthieu.moy@grenoble-inp.fr","sentAt":"2014-08-29T06:44:09Z","receivedAt":"2014-08-29T06:44:09Z","isPatch":true,"sender":{"key":"matthieu.moy@grenoble-inp.fr","avatar":"https://gravatar.com/avatar/72c8a2705971a25dfaff23cece15130d405685845d911aedd5667ace277f3fc5?d=mp&s=160"},"body":"Junio C Hamano writes:\n\n> Here is how I phrased in the one queued tentatively.\n\nOK with me, thanks,\n\n-- \nMatthieu Moy\nhttp://www-verimag.imag.fr/~moy/\n"}]}