[Dune] [Dune-Commit] dune-grid r8137 - trunk/dune/grid/common/refinement

Oliver Sander sander at mi.fu-berlin.de
Wed May 23 07:47:51 CEST 2012

Am 23.05.2012 01:19, schrieb Jö Fahlke:
> Am Tue, 22. May 2012, 21:26:04 +0200 schrieb Oliver Sander:
>> after seeing this patch I started grepping for editor hints out
>> of curiosity.  In dune/grid/common alone there are three different
>> varieties.  Which one is correct?
> By varieties I assume you mean different values for e.g. the indentation
> width.  In that case it depends on the file, since some files were obviously
> created with an indentation of 2 while others were obviously created with an
> intedation of 4.  The intend of the editor hints then is to keep the same
> indentation depth, i.e. make sure the next perseon editing that file doesn't
> instoduce parts with a different indentation depth.
> Of course, some files already have mixed indentation depth, in that case I
> just try to figure out which one is dominant or choose one at random, and hope
> it will prevail in the long run...
Thanks for the information.  I had assumed that we were aiming at 
across all files.

More information about the Dune mailing list