From: Daniel Arndt Date: Sat, 3 Sep 2016 18:00:40 +0000 (+0200) Subject: Merge pull request #3058 from drwells/ignore-global-indent-options X-Git-Tag: v8.5.0-rc1~710 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=19a6f9fa5950537a122de7b68be0753dc3ad16a8;p=dealii.git Merge pull request #3058 from drwells/ignore-global-indent-options Set --options=none when indenting .inst.in files. --- 19a6f9fa5950537a122de7b68be0753dc3ad16a8