diff options
| author | David Aspinall | 2004-08-25 20:20:24 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-08-25 20:20:24 +0000 |
| commit | 1b0a9f62c9ea2e577a72ecf1c180713471b965fb (patch) | |
| tree | af8c16501e9af3f8a866693bf391446650cb2f1b /pgshell | |
| parent | 64a4e312f60d0a9255efe880d1d05efc4c06e5f5 (diff) | |
Add pg-internal-warning. Use display-warning for that and proof-debug, if available.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions