diff --git a/org.eventb.texteditor.feature/.settings/org.eclipse.core.resources.prefs b/org.eventb.texteditor.feature/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 0000000000000000000000000000000000000000..99f26c0203a7844de00dbfc56e6a35d8ed3c022c --- /dev/null +++ b/org.eventb.texteditor.feature/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/<project>=UTF-8 diff --git a/org.eventb.texteditor.feature/.settings/org.eclipse.core.runtime.prefs b/org.eventb.texteditor.feature/.settings/org.eclipse.core.runtime.prefs new file mode 100644 index 0000000000000000000000000000000000000000..5a0ad22d2a76684139fad95f6b8d209c7cd0d078 --- /dev/null +++ b/org.eventb.texteditor.feature/.settings/org.eclipse.core.runtime.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +line.separator=\n diff --git a/org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs b/org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs deleted file mode 100644 index c5bb45432ab941c41f76cd9da72eea66a1d4361a..0000000000000000000000000000000000000000 --- a/org.eventb.texteditor.feature/.settings/org.eclipse.jdt.core.prefs +++ /dev/null @@ -1,13 +0,0 @@ -# -#Wed Jun 25 10:22:53 CEST 2014 -org.eclipse.jdt.core.compiler.debug.localVariable=generate -org.eclipse.jdt.core.compiler.compliance=1.8 -org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve -org.eclipse.jdt.core.compiler.debug.sourceFile=generate -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 -org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.debug.lineNumber=generate -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled -org.eclipse.jdt.core.compiler.source=1.8 -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error diff --git a/org.eventb.texteditor.parsers/.settings/org.eclipse.core.resources.prefs b/org.eventb.texteditor.parsers/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 0000000000000000000000000000000000000000..99f26c0203a7844de00dbfc56e6a35d8ed3c022c --- /dev/null +++ b/org.eventb.texteditor.parsers/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/<project>=UTF-8 diff --git a/org.eventb.texteditor.parsers/.settings/org.eclipse.core.runtime.prefs b/org.eventb.texteditor.parsers/.settings/org.eclipse.core.runtime.prefs new file mode 100644 index 0000000000000000000000000000000000000000..5a0ad22d2a76684139fad95f6b8d209c7cd0d078 --- /dev/null +++ b/org.eventb.texteditor.parsers/.settings/org.eclipse.core.runtime.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +line.separator=\n diff --git a/org.eventb.texteditor.parsers/.settings/org.eclipse.jdt.core.prefs b/org.eventb.texteditor.parsers/.settings/org.eclipse.jdt.core.prefs deleted file mode 100644 index f42de363afaae68bbd968318f1d331877f5514fc..0000000000000000000000000000000000000000 --- a/org.eventb.texteditor.parsers/.settings/org.eclipse.jdt.core.prefs +++ /dev/null @@ -1,7 +0,0 @@ -eclipse.preferences.version=1 -org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled -org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7 -org.eclipse.jdt.core.compiler.compliance=1.7 -org.eclipse.jdt.core.compiler.problem.assertIdentifier=error -org.eclipse.jdt.core.compiler.problem.enumIdentifier=error -org.eclipse.jdt.core.compiler.source=1.7 diff --git a/org.eventb.texteditor.ui/.settings/org.eclipse.core.resources.prefs b/org.eventb.texteditor.ui/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 0000000000000000000000000000000000000000..99f26c0203a7844de00dbfc56e6a35d8ed3c022c --- /dev/null +++ b/org.eventb.texteditor.ui/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/<project>=UTF-8 diff --git a/org.eventb.texteditor.ui/.settings/org.eclipse.core.runtime.prefs b/org.eventb.texteditor.ui/.settings/org.eclipse.core.runtime.prefs new file mode 100644 index 0000000000000000000000000000000000000000..5a0ad22d2a76684139fad95f6b8d209c7cd0d078 --- /dev/null +++ b/org.eventb.texteditor.ui/.settings/org.eclipse.core.runtime.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +line.separator=\n diff --git a/org.eventb.texttools/.settings/org.eclipse.core.resources.prefs b/org.eventb.texttools/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 0000000000000000000000000000000000000000..99f26c0203a7844de00dbfc56e6a35d8ed3c022c --- /dev/null +++ b/org.eventb.texttools/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/<project>=UTF-8 diff --git a/org.eventb.texttools/.settings/org.eclipse.core.runtime.prefs b/org.eventb.texttools/.settings/org.eclipse.core.runtime.prefs new file mode 100644 index 0000000000000000000000000000000000000000..5a0ad22d2a76684139fad95f6b8d209c7cd0d078 --- /dev/null +++ b/org.eventb.texttools/.settings/org.eclipse.core.runtime.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +line.separator=\n