diff options
Diffstat (limited to 'src/parser/input.h')
| -rw-r--r-- | src/parser/input.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/parser/input.h b/src/parser/input.h index 6ed9bb441..b9123fc45 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -94,10 +94,11 @@ class CVC4_PUBLIC Input { InputStream *d_inputStream; /* Since we own d_inputStream and it needs to be freed, we need to prevent - * copy construction and assignment. + * copy construction and assignment. Mark them private and do not define + * them. */ - Input(const Input& input) { Unimplemented("Copy constructor for Input."); } - Input& operator=(const Input& input) { Unimplemented("operator= for Input."); } + Input(const Input& input) CVC4_UNUSED; + Input& operator=(const Input& input) CVC4_UNUSED; public: |