diff --git a/.gitattributes b/.gitattributes index 85087c8e0fe5c13b5551e69e24c641fd9c5c1ee1..5cb0f7baf1bc6167712307b9f68d40c9566937e7 100644 --- a/.gitattributes +++ b/.gitattributes @@ -10,9 +10,6 @@ /bench/encoding/ export-ignore /examples/in_progress/ export-ignore -/examples/multiprecision/random/ export-ignore -/examples/multiprecision/bench-include/ export-ignore -/examples/multiprecision/mini-gmp/ export-ignore /misc/ export-ignore /opam/ export-ignore /tests/ export-ignore diff --git a/examples/multiprecision/.gitattributes b/examples/multiprecision/.gitattributes new file mode 100644 index 0000000000000000000000000000000000000000..a179b5909470d542504515db138b4ba12c72045d --- /dev/null +++ b/examples/multiprecision/.gitattributes @@ -0,0 +1,3 @@ +random/ export-ignore +bench-include/ export-ignore +mini-gmp/ export-ignore \ No newline at end of file