(core) remove metrics

Summary: This removes some old metric code. There's also a user preference dialog that has a single option (whether to allow metrics) this is left in place with a dummy option. It could be ripped out as well, probably.

Test Plan: existing tests pass

Reviewers: dsagal

Reviewed By: dsagal

Differential Revision: https://phab.getgrist.com/D2622

app/server/mergedServerMain.ts

@@ -34,7 +34,6 @@ interface ServerOptions extends FlexServerOptions {
   logToConsole?: boolean;  // If set, messages logged to console (default: false)
                            //   (but if options are not given at all in call to main,
                            //    logToConsole is set to true)
-  metrics?: boolean;       // If set, metric collector is enabled (default: true)
   s3?: boolean;            // If set, documents saved to s3 (default is to check environment
                            // variables, which get set in various ways in dev/test entry points)
 }
@@ -131,10 +130,6 @@ export async function main(port: number, serverTypes: ServerType[],
     await server.addDoc();
   }
 
-  if (options.metrics === false && includeDocs) {
-    server.disableMetrics();
-  }
-
   server.finalize();
 
   server.summary();