Commit 049da08a22b0ca6d63d2be6c209da5ac1335365c

Anthony Green 2019-11-23T07:44:26

Add dejagnu directives accidentally removed