Remove codet::move

tautschnig · tautschnig · commit 75ade046b944 · 2018-11-05T15:02:56.000Z
With the preceding changes it is no longer being used.
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -137,11 +137,6 @@ class code_blockt:public codet
     operands()=std::move((std::vector<exprt> &&)_statements);
   }
 
-  void move(codet &code)
-  {
-    move_to_operands(code);
-  }
-
   void add(const codet &code)
   {
     add_to_operands(code);

Original file line number	Diff line number	Diff line change
`@@ -137,11 +137,6 @@ class code_blockt:public codet`
`137`	`137`	`operands()=std::move((std::vector<exprt> &&)_statements);`
`138`	`138`	`}`
`139`	`139`
`140`		`- void move(codet &code)`
`141`		`- {`
`142`		`- move_to_operands(code);`
`143`		`- }`
`144`		`-`
`145`	`140`	`void add(const codet &code)`
`146`	`141`	`{`
`147`	`142`	`add_to_operands(code);`