Remove dev/migratedoc.tex

[fingolfin]

We already have doc/tut/migrat.xml

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 78.87%. Comparing base (8187e9e) to head (72ec0df).
⚠️ Report is 1 commits behind head on master.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #6431      +/-   ##
==========================================
- Coverage   78.87%   78.87%   -0.01%     
==========================================
  Files         685      685              
  Lines      293550   293549       -1     
  Branches     8672     8672              
==========================================
- Hits       231530   231528       -2     
  Misses      60211    60211              
- Partials     1809     1810       +1     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[ThomasBreuer]

We already have doc/tut/migrat.xml

Comparing doc/tut/migrat.xml with dev/migratedoc.tex, one finds that some statements are commented out in the latter file which are not true anymore. In this sense, dev/migratedoc.tex is in a better shape.

The material described in the two files is interesting at most for historical reasons. Is it still mentioned somewhere in the manual or in the GAP web pages?

[fingolfin]

OK I wasn't aware that doc/tut/migrat.xml is also not used. So I could remove it as well...

I am not aware of any place mentioning this information. It might be useful to put it somewhere, but where? One could also argue it is still there in the repository... but nobody will find it there who doesn't already at least suspect it exists...

[ThomasBreuer]

If doc/tut/migrat.xml and dev/migratedoc.tex are not mentioned in the current GAP documentation then they can be removed from the repository.