diff options
| author | Stephane Glondu <steph@glondu.net> | 2019-08-02 10:21:09 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2019-08-02 10:21:09 +0200 |
| commit | 82c5c53b499b5353e9bdc60e5cc2118b0812fe89 (patch) | |
| tree | 7d9c0cf5b77a58e0af2d3b4ec3c1fe2fd3aac5bc | |
| parent | 7c05a449e69a76d154c08bb97473a87437c5b897 (diff) | |
Remove changes in upstream sources to please dgitdebian/4.1.2-4
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | src/rpc-generator/config.ml | 1 |
2 files changed, 1 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore deleted file mode 100644 index 845ca067..00000000 --- a/.gitignore +++ /dev/null @@ -1 +0,0 @@ -.pc diff --git a/src/rpc-generator/config.ml b/src/rpc-generator/config.ml new file mode 100644 index 00000000..b713c9ff --- /dev/null +++ b/src/rpc-generator/config.ml @@ -0,0 +1 @@ +let cpp = "cpp";; |