Using delete to forbid copies of objects

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.h

@@ -47,8 +47,9 @@ class java_string_library_preprocesst:public messaget
   bool is_known_string_type(irep_idt class_name);
 
 private:
-  // We forbid copies of the object by making the copy operator private.
-  java_string_library_preprocesst(const java_string_library_preprocesst &);
+  // We forbid copies of the object
+  java_string_library_preprocesst(
+    const java_string_library_preprocesst &)=delete;
 
   static bool java_type_matches_tag(const typet &type, const std::string &tag);
   static bool is_java_string_pointer_type(const typet &type);