*** empty log message ***

[splint.git] / src / Headers / flagSpec.h

diff --git a/src/Headers/flagSpec.h b/src/Headers/flagSpec.h
index c55ccfc9ad2c467fbf60b76ba32b489d07a43005..fc35025c604c0f34202744f7af4686f74e596fc5 100644 (file)
--- a/src/Headers/flagSpec.h
+++ b/src/Headers/flagSpec.h
@@ -35,6 +35,7 @@ extern /*@only@*/ flagSpec flagSpec_createPlain (/*@only@*/ cstring) ;
 extern /*@only@*/ flagSpec 
    flagSpec_createOr (/*@only@*/ cstring, /*@only@*/ flagSpec) ;
 
+extern /*@only@*/ flagSpec flagSpec_copy (flagSpec) /*@*/ ;
 extern /*@unused@*/ /*@only@*/ cstring flagSpec_unparse (flagSpec) /*@*/ ;
 extern void flagSpec_free (/*@only@*/ flagSpec) ;