disable automatic formatting of Java code blocks in comments/JavaDoc

KeYProject · Dec 5, 2024 · 9556c88 · 9556c88
1 parent 6926058
commit 9556c88
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/tools/checkstyle/keyCodeStyle.xml b/scripts/tools/checkstyle/keyCodeStyle.xml
@@ -106,7 +106,7 @@
         <setting id="org.eclipse.jdt.core.formatter.comment.format_html" value="true"/>
         <setting id="org.eclipse.jdt.core.formatter.comment.format_javadoc_comments" value="true"/>
         <setting id="org.eclipse.jdt.core.formatter.comment.format_line_comments" value="true"/>
-        <setting id="org.eclipse.jdt.core.formatter.comment.format_source_code" value="true"/>
+        <setting id="org.eclipse.jdt.core.formatter.comment.format_source_code" value="false"/>
         <setting id="org.eclipse.jdt.core.formatter.comment.indent_parameter_description" value="false"/>
         <setting id="org.eclipse.jdt.core.formatter.comment.indent_root_tags" value="true"/>
         <setting id="org.eclipse.jdt.core.formatter.comment.indent_tag_description" value="false"/>